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 (91)
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 ⋮ ACoRe: automated goal-conflict resolution ⋮ Canonicity of proofs in constructive modal logic ⋮ Model checking timed recursive CTL ⋮ Finite-state concurrent programs can be expressed in pairwise normal form ⋮ On the verification of detectability for timed discrete event systems ⋮ Automated temporal reasoning about reactive systems ⋮ An automata-theoretic approach to linear temporal logic ⋮ Realizability of Concurrent Recursive Programs ⋮ Model checking for hybrid branching-time logics ⋮ Efficient reactive synthesis using mode decomposition ⋮ First order Büchi automata and their application to verification of LTL specifications ⋮ Coalgebraic CTL: fixpoint characterization and polynomial-time model checking ⋮ 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
This page was built for publication: Using branching time temporal logic to synthesize synchronization skeletons
