Design and synthesis of synchronization skeletons using branching time temporal logic. (English) Zbl 0546.68014

Logics of programs, Workshop Yorktown Heights/NY 1981, Lect. Notes Comput. Sci. 131, 52-71 (1982).
[For the entire collection see Zbl 0477.00026.]
A method for constructing concurrent programs is proposed, in which the synchronisation skeleton of the program is automatically synthesized from a specification given by a formula \(f\) in a propositional branching time logic. If the specification is consistent (i.e. if \(f\) is satisfiable) a tableau-based decision procedure gives a finite model for \(f\), from which the synchronisation skeleton of a program meeting the specification can be read. [A revised version of the paper can be found in Sci. Comput. Program. 2, 241–266 (1982; Zbl 0514.68032).]
Reviewer: H.Fuss and E.Smith


68N25 Theory of operating systems
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)