Deciding full branching time logic
From MaRDI portal
Publication:3722471
DOI10.1016/S0019-9958(84)80047-9zbMath0593.03007OpenAlexW2072887965MaRDI QIDQ3722471
A. P. Sistla, E. Allen Emerson
Publication date: 1984
Published in: Information and Control (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0019-9958(84)80047-9
Modal logic (including the logic of norms) (03B45) Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25)
Related Items (58)
CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ A branching time logic with past operators ⋮ Verification and comparison of transition systems ⋮ Church's Problem Revisited ⋮ Specification and Verification of Multi-Agent Systems ⋮ Automata-theoretic techniques for modal logics of programs ⋮ Temporal Logic and Fair Discrete Systems ⋮ Deciding $$\mathsf {ATL^*}$$ Satisfiability by Tableaux ⋮ A Tableau for Bundled Strategies ⋮ A decision procedure for combinations of propositional temporal logic and other specialized theories ⋮ Determinization and memoryless winning strategies ⋮ TTL : a formalism to describe local and global properties of distributed systems ⋮ Uniform inevitability is tree automaton ineffable ⋮ A transformation-based synthesis of temporal specification ⋮ Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic ⋮ A clausal resolution method for branching-time logic \(\text{ECTL}^+\) ⋮ Logic programming approach to automata-based decision procedures ⋮ Characterizing finite Kripke structures in propositional temporal logic ⋮ An optimal decision procedure for right propositional neighborhood logic ⋮ To be fair, use bundles ⋮ A propositional probabilistic logic with discrete linear time for reasoning about evidence ⋮ Axiomatising extended computation tree logic ⋮ Expressiveness and succinctness of a logic of robustness ⋮ Completeness of a branching-time logic with possible choices ⋮ A tableau-based decision procedure for CTL\(^*\) ⋮ Complexity of synthesis of composite service with correctness guarantee ⋮ \textit{Once} and \textit{for all} ⋮ Linear temporal logic symbolic model checking ⋮ TABLEAUX: A general theorem prover for modal logics ⋮ Sublogics of a branching time logic of robustness ⋮ Axiomatising extended computation tree logic ⋮ A model checker for linear time temporal logic ⋮ Inconsistency-tolerant temporal reasoning with hierarchical information ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ An axiomatization of full Computation Tree Logic ⋮ Model Theoretic Syntax and Parsing ⋮ An Automata-based Approach for CTL⋆ With Constraints ⋮ A Decision Procedure for CTL* Based on Tableaux and Automata ⋮ A clausal resolution method for extended computation tree logic ECTL ⋮ Automata on infinite objects and their applications to logic and programming ⋮ A clausal resolution method for CTL branching-time temporal logic ⋮ CTL\(^\ast\) with graded path modalities ⋮ A Labeled Natural Deduction System for a Fragment of CTL * ⋮ Unnamed Item ⋮ Incremental reasoning on monadic second-order logics with logic programming ⋮ From LTL to Symbolically Represented Deterministic Automata ⋮ Büchi Complementation and Size-Change Termination ⋮ Temporal Logics with Reference Pointers and Computation Tree Logics ⋮ A Rooted Tableau for BCTL* ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ Decidability and Expressivity of Ockhamist Propositional Dynamic Logics ⋮ An axiomatization of PCTL* ⋮ Verification of multi-agent systems with public actions against strategy logic ⋮ Branching time agents logics, satisfiability problem by rules in reduced form ⋮ Relating word and tree automata ⋮ Module checking ⋮ A logic with revocable and refinable strategies ⋮ A goal-directed decision procedure for hybrid PDL
This page was built for publication: Deciding full branching time logic
