Synthesis of Communicating Processes from Temporal Logic Specifications

DOI10.1145/357233.357237zbMath0522.68030MaRDI QIDQ3673090

Zohar Manna, Pierre Wolper

Publication date: 1984

Published in: ACM Transactions on Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/357233.357237

zbMATH Keywords

synchronization; concurrency; specification; mutual exclusion; propositional temporal logic; PTL

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

68Q85: Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

03B44: Temporal logic

Related Items

Decidability and incompleteness results for first-order temporal logics of linear time, Converting a Büchi alternating automaton to a usual nondeterministic one, Factorisation of finite state machines under strong and observational equivalences, Control machines: A new model of parallelism for compositional specifications and their effective compilation, Resolution for some first-order modal systems, TABLEAUX: A general theorem prover for modal logics, The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\), On undecidability of propositional temporal logics on trace systems, Proving partial order properties, Fair Petri nets and structural induction for rings of processes, A temporal logic-based approach for the description of object behavior evolution, Verification by augmented finitary abstraction, Inductive synthesis of recursive processes from logical properties, MetateM: An introduction, From complementation to certification, TTL : a formalism to describe local and global properties of distributed systems