The temporal logic of branching time
From MaRDI portal
Publication:789895
DOI10.1007/BF01257083zbMath0533.68036MaRDI QIDQ789895
Mordechai Ben-Ari, Zohar Manna, Amir Pnueli
Publication date: 1983
Published in: Acta Informatica (Search for Journal in Brave)
finite model propertytemporal logicreasoning about programsbranching operatorscompleteness of an axiomatizationexponential decision procedure for satisfiabilitytree of all possible computations
Related Items (56)
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL + ⋮ Completeness and decidability results for CTL in constructive type theory ⋮ Axiomatization of a branching time logic with indistinguishability relations ⋮ A propositional dense time logic ⋮ Temporal Logic and Fair Discrete Systems ⋮ Interleaving set temporal logic ⋮ TTL : a formalism to describe local and global properties of distributed systems ⋮ Synthesis of communicating process skeletons from temporal-spatial logic specifications ⋮ A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations ⋮ Characterizing finite Kripke structures in propositional temporal logic ⋮ To be fair, use bundles ⋮ Temporal Specifications with Accumulative Values ⋮ One-Pass Tableaux for Computation Tree Logic ⋮ Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL ⋮ Model checking open systems with alternating projection temporal logic ⋮ Branching vs. Linear Time: Semantical Perspective ⋮ The Birth of Model Checking ⋮ DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC ⋮ SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR ⋮ Branching versus linear logics yet again ⋮ Proving correctness of labeled transition systems by semantic tableaux ⋮ Proof systems for satisfiability in Hennessy-Milner logic with recursion ⋮ Unnamed Item ⋮ SnS can be modally characterized ⋮ Mathematical modal logic: A view of its evolution ⋮ A propositional linear time logic with time flow isomorphic to \(\omega^2\) ⋮ A tableau calculus for first-order branching time logic ⋮ TABLEAUX: A general theorem prover for modal logics ⋮ Deductive verification of alternating systems ⋮ A hierarchy of temporal logics with past ⋮ Formal timing analysis of distributed systems ⋮ One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ The modeling library of eavesdropping methods in quantum cryptography protocols by model checking ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ The expressive power of implicit specifications ⋮ A multiset-based model of synchronizing agents: Computability and robustness ⋮ Model Theoretic Syntax and Parsing ⋮ Characterizing CTL-like logics on finite trees. ⋮ Meanings of Model Checking ⋮ Encapsulating deontic and branching time specifications ⋮ \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\) ⋮ Automatic and hierarchical verification for concurrent systems ⋮ Quantifying Bounds in Strategy Logic ⋮ An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability ⋮ On the Complexity of Branching-Time Logics ⋮ Branching-time logics repeatedly referring to states ⋮ The temporal logic of branching time ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ A multiprocess network logic with temporal and spatial modalities ⋮ An infinite hierarchy of temporal logics over branching time ⋮ Exogenous Probabilistic Computation Tree Logic ⋮ Quantitative program logic and expected time bounds in probabilistic distributed algorithms. ⋮ On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic ⋮ A goal-directed decision procedure for hybrid PDL ⋮ A Compositional Automata-based Approach for Model Checking Multi-Agent Systems
Cites Work
This page was built for publication: The temporal logic of branching time
