Synthesis of Communicating Processes from Temporal Logic Specifications

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (46)

Compositional Control Synthesis for Partially Observable Systems
Hierarchical verification using verification diagrams
Automated temporal reasoning about reactive systems
Specification and verification of database dynamics
Decidability and incompleteness results for first-order temporal logics of linear time
Towards a notion of unsatisfiable and unrealizable cores for LTL
Inferring Synchronization under Limited Observability
Characterizing finite Kripke structures in propositional temporal logic
Synthesis of communicating process skeletons from temporal-spatial logic specifications
Supervisory control and reactive synthesis: a comparative introduction
Automated synthesis of asynchronizations
Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\)
Maintenance goals of agents in a dynamic environment: formulation and policy construction
A decision procedure for combinations of propositional temporal logic and other specialized theories
Synthesis of Reactive(1) designs
Defining, analysing and implementing communication protocols using attribute grammars
Factorisation of finite state machines under strong and observational equivalences
On undecidability of propositional temporal logics on trace systems
Unifying models
Submodule construction as equation solving in CCS
Proving partial order properties
MetateM: An introduction
Synchronous counting and computational algorithm design
Construction of deterministic transition graphs from dynamic integrity constraints
Decidability for a temporal logic used in discrete-event system analysis
Graph Games and Reactive Synthesis
The complexity of reasoning about knowledge and time. I: Lower bounds
Control machines: A new model of parallelism for compositional specifications and their effective compilation
Resolution for some first-order modal systems
Verification by augmented finitary abstraction
Theoretical foundations of handling large substitution sets in temporal integrity monitoring
Transformation of dynamic integrity constraints into transaction specifications
Synthesis of large dynamic concurrent programs from dynamic specifications
Property-oriented expansion
Converting a Büchi alternating automaton to a usual nondeterministic one
The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\)
Fair Petri nets and structural induction for rings of processes
A temporal logic-based approach for the description of object behavior evolution
TABLEAUX: A general theorem prover for modal logics
From complementation to certification
Reactive synthesis from interval temporal logic specifications
Inductive synthesis of recursive processes from logical properties
ACoRe: automated goal-conflict resolution
An automata-theoretic approach to linear temporal logic
TTL : a formalism to describe local and global properties of distributed systems
Complementing deterministic Büchi automata in polynomial time

This page was built for publication: Synthesis of Communicating Processes from Temporal Logic Specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3673090)