Many-sorted temporal logic for multi-processes systems. (English) Zbl 0558.68026

Mathematical foundations of computer science, Proc. 11th Symp., Praha/Czech. 1984, Lect. Notes Comput. Sci. 176, 273-281 (1984).
[For the entire collection see Zbl 0544.00022.]
The paper presents a basic formal frame for a temporal logic in which every process defines a local time and a local temporal logic, and the global time and logic are obtained by a composition of local times and logics. The temporal logic introduced is many-sorted in which propositional variables and modal operators are typed and every process is assigned a certain type. Examples of application of the logic introduced are also shown: one for the so-called maximum semantics requiring that processes should not be lazy, and the other for nets of processes communicating by buffers.
Reviewer: J.Zlatu┼íka


68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)


Zbl 0544.00022