A temporal logic approach to specify and to prove properties of finite state concurrent systems. (English) Zbl 0746.68030

Danelutto, M.; Masini, A.

CSL ’88, Proc. 2nd Workshop, Duisburg/FRG 1988, Lect. Notes Comput. Sci. 385, 63-79 (1989).

[For the entire collection see Zbl 0709.00020.]
Concurrent systems are considered which are in fact finite collections of asynchronous interacting finite transition systems. The behavior of such a system CS is proposed to describe in terms of the propositional logic UB of branching time, with atomary propositions denoting states (or actions, in another interpretation ) of components of CS. There are two kinds of axioms. Axioms of the first kind (corresponding to transition relations of components of CS) refer to local times of components and define possible next states for (current) states of components. Axioms of the second kind refer to the global time of CS and define some constraints on global states and possible execution paths of CS. Among these constraints are, f.e., \(\forall G(\neg(p\& q))\) (mutual exclusion of states \(p\) and \(q\)), \(\neg p\&\neq q\supset\forall X(\neg q)\) which expresses (taken as an axiom what is equivalent to its closure under \(\forall G\), but not by itself as it can be understood from the authors’ comments) that if \(p\) and \(q\) are false in a global state then in all the execution paths \(p\) must become true before \(q\). Using these axioms the axioms of the first kind are translated to axioms referring to the global time of CS. The main theorem (given without proofs) asserts (as I understand it from the authors’ rather vague formulation) that a formula of UB can be deduced from these axioms iff it is valid in a finite model effectively constructible from these axioms. In the second part of the paper an algorithm is described which checks satisfiability of formulas of UB in finite models. It is noted that the algorithm is implemented on a SUN-3 workstation.

Reviewer: M.Val’ev

MSC:

68Q10	Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
03B70	Logic in computer science
03B45	Modal logic (including the logic of norms)
68Q60	Specification and verification (program logics, model checking, etc.)

Keywords:

concurrent transition systems; propositional temporal logic; model checking

Citations:

Zbl 0709.00020