Using branching time temporal logic to synthesize synchronization skeletons
From MaRDI portal
Publication:1051419
DOI10.1016/0167-6423(83)90017-5zbMath0514.68032OpenAlexW2048355938MaRDI QIDQ1051419
Edmund M. Clarke, E. Allen Emerson
Publication date: 1982
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0167-6423(83)90017-5
Related Items
Completeness and decidability results for CTL in constructive type theory, Axiomatization of a branching time logic with indistinguishability relations, A logic of separating modalities, Church's Problem Revisited, Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP, Complexity results on branching-time pushdown model checking, A logic for reasoning about time and reliability, Temporal Logic and Fair Discrete Systems, Combining Model Checking and Deduction, Graph Games and Reactive Synthesis, Operational semantics of Framed Tempura, Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems, A decision procedure for combinations of propositional temporal logic and other specialized theories, TTL : a formalism to describe local and global properties of distributed systems, MetateM: An introduction, On temporal logics with data variable quantifications: decidability and complexity, Synthesis of large dynamic concurrent programs from dynamic specifications, Linear templates of ACTL formulas with an application to SAT-based verification, Control problems in a temporal logic framework, The complexity of reasoning about knowledge and time. I: Lower bounds, On Abstraction of Probabilistic Systems, From model checking to equilibrium checking: reactive modules for rational verification, Automata-theoretic decision of timed games, Temporal Specifications with Accumulative Values, MR4UM: a framework for adding fault tolerance to UML state diagrams, Preface to the special issue: Temporal logics of agency, To be announced, A survey on temporal logics for specifying and verifying real-time systems, Taming strategy logic: non-recurrent fragments, The tail-recursive fragment of timed recursive CTL, A quadratic construction for Zielonka automata with acyclic communication structure, Model and program repair via group actions, Completeness of a branching-time logic with possible choices, Satisfiability of quantitative probabilistic CTL: rise to the challenge, Supervisory control and reactive synthesis: a comparative introduction, Analysing AWN-Specifications Using mCRL2 (Extended Abstract), A tableau-based decision procedure for CTL\(^*\), Towards a notion of unsatisfiable and unrealizable cores for LTL, Theorem proving using clausal resolution: from past to present, Complexity of synthesis of composite service with correctness guarantee, Synthesis from scenario-based specifications, On hierarchically developing reactive systems, Unnamed Item, Unnamed Item, A propositional linear time logic with time flow isomorphic to \(\omega^2\), CTL update of Kripke models through protections, Deductive verification of alternating systems, Automatic Data-Abstraction in Model Checking Multi-Agent Systems, Sublogics of a branching time logic of robustness, Measuring inconsistency in some branching time logics, On the expressive power of hybrid branching-time logics, Temporal Logic with Recursion., One-pass Context-based Tableaux Systems for CTL and ECTL, Rewrite rules for \(\mathrm{CTL}^\ast\), On undecidability of propositional temporal logics on trace systems, Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\), Finite-state concurrent programs can be expressed succinctly in triple normal form, SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS, Performability assessment by model checking of Markov reward models, Ensuring liveness properties of distributed systems: open problems, Decision procedures and expressiveness in the temporal logic of branching time, Symbolic model checking with rich assertional languages, Unnamed Item, Terminating Tableaux for Hybrid Logic with Eventualities, A modular approach to defining and characterising notions of simulation, Games for Temporal Logics on Trees, Fifty years of Hoare's logic, Finite-state concurrent programs can be expressed in pairwise normal form, Realizability of Concurrent Recursive Programs, Model checking for hybrid branching-time logics, Submodule construction as equation solving in CCS, Temporal logic with recursion, Constructive Formalization of Hybrid Logic with Eventualities, A Logic for Rewriting Strategies, Differential dynamic logic for hybrid systems, Automating the addition of fault tolerance with discrete controller synthesis, Model checking for hybrid logic, Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models, Compositional verification of asynchronous concurrent systems using CADP, Probabilistic Temporal Logics, Proving partial order properties, A theory of timed automata
