Synthesis of Communicating Processes from Temporal Logic Specifications
From MaRDI portal
Publication:3673090
DOI10.1145/357233.357237zbMath0522.68030OpenAlexW2040127143MaRDI QIDQ3673090
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
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Temporal logic (03B44)
Related Items (42)
Unifying models ⋮ Specification and verification of database dynamics ⋮ Fair Petri nets and structural induction for rings of processes ⋮ Graph Games and Reactive Synthesis ⋮ A decision procedure for combinations of propositional temporal logic and other specialized theories ⋮ Decidability and incompleteness results for first-order temporal logics of linear time ⋮ A temporal logic-based approach for the description of object behavior evolution ⋮ Compositional Control Synthesis for Partially Observable Systems ⋮ TTL : a formalism to describe local and global properties of distributed systems ⋮ Maintenance goals of agents in a dynamic environment: formulation and policy construction ⋮ MetateM: An introduction ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Complementing deterministic Büchi automata in polynomial time ⋮ Synthesis of communicating process skeletons from temporal-spatial logic specifications ⋮ The complexity of reasoning about knowledge and time. I: Lower bounds ⋮ Characterizing finite Kripke structures in propositional temporal logic ⋮ Synchronous counting and computational algorithm design ⋮ Supervisory control and reactive synthesis: a comparative introduction ⋮ Automated synthesis of asynchronizations ⋮ Construction of deterministic transition graphs from dynamic integrity constraints ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Synthesis of Reactive(1) designs ⋮ Theoretical foundations of handling large substitution sets in temporal integrity monitoring ⋮ Transformation of dynamic integrity constraints into transaction specifications ⋮ Defining, analysing and implementing communication protocols using attribute grammars ⋮ 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 ⋮ Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\) ⋮ Decidability for a temporal logic used in discrete-event system analysis ⋮ Converting a Büchi alternating automaton to a usual nondeterministic one ⋮ Inferring Synchronization under Limited Observability ⋮ Submodule construction as equation solving in CCS ⋮ Reactive synthesis from interval temporal logic specifications ⋮ From complementation to certification ⋮ Verification by augmented finitary abstraction ⋮ Inductive synthesis of recursive processes from logical properties ⋮ Proving partial order properties ⋮ Property-oriented expansion
This page was built for publication: Synthesis of Communicating Processes from Temporal Logic Specifications
