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

Enjalbert, P.; Michel, M.

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

MSC:

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

Keywords:

many-sorted logic; types; parallelism; temporal logic; maximum semantics; processes

Citations:

Zbl 0544.00022