## 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

### MSC:

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

### Citations:

Zbl 0477.00026; Zbl 0514.68032