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
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
