Decision procedures and expressiveness in the temporal logic of branching time

DOI10.1016/0022-0000(85)90001-7zbMath0559.68051OpenAlexW2067441543WikidataQ56432687 ScholiaQ56432687MaRDI QIDQ2265816

Publication date: 1985

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(85)90001-7

zbMATH Keywords

completeness satisfiability computation tree logic complete axiomatization CTL exponential decision procedure relative expressive power small model theorem UB unified branching time logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15)

Related Items (98)

Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL ⁺ ⋮ Parametrised Complexity of Satisfiability in Temporal Logic ⋮ A logical query language for hypermedia systems ⋮ Completeness and decidability results for CTL in constructive type theory ⋮ Church's Problem Revisited ⋮ A logic to reason about likelihood ⋮ Automata-theoretic techniques for modal logics of programs ⋮ Deadness and how to disprove liveness in hybrid dynamical systems ⋮ Sequent calculi for branching time temporal logics of knowledge and beliefwith awareness: completeness and decidability ⋮ Temporal Logic and Fair Discrete Systems ⋮ Interpreting logics of knowledge in propositional dynamic logic ⋮ Deontic action logic, atomic Boolean algebras and fault-tolerance ⋮ Branching Time? Pruning Time! ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ Complexity of finite-variable fragments of propositional temporal and modal logics of computation ⋮ Interleaving set temporal logic ⋮ Determinization and memoryless winning strategies ⋮ TTL : a formalism to describe local and global properties of distributed systems ⋮ Reasoning about equilibria in game-like concurrent systems ⋮ Multiagent temporal logics, unification problems, and admissibilities ⋮ A clausal resolution method for branching-time logic \(\text{ECTL}^+\) ⋮ A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations ⋮ The complexity of reasoning about knowledge and time. I: Lower bounds ⋮ Branching-time logics and fairness, revisited ⋮ An optimal decision procedure for right propositional neighborhood logic ⋮ To be fair, use bundles ⋮ Unnamed Item ⋮ Branching-time logics with path relativisation ⋮ Axiomatising extended computation tree logic ⋮ One-Pass Tableaux for Computation Tree Logic ⋮ To be announced ⋮ Mechanising Gödel-Löb provability logic in HOL light ⋮ Dynamic temporal logical operations in multi-agent logics ⋮ Taming strategy logic: non-recurrent fragments ⋮ Fuzzy Halpern and Shoham's interval temporal logics ⋮ Completeness of a branching-time logic with possible choices ⋮ Reasoning About Substructures and Games ⋮ A tableau-based decision procedure for CTL\(^*\) ⋮ Completeness for flat modal fixpoint logics ⋮ \textit{Once} and \textit{for all} ⋮ Unnamed Item ⋮ A uniform method for proving lower bounds on the computational complexity of logical theories ⋮ Mathematical modal logic: A view of its evolution ⋮ Decidability of an Xstit logic ⋮ The expressibility of fragments of hybrid graph logic on finite digraphs ⋮ A propositional linear time logic with time flow isomorphic to \(\omega^2\) ⋮ Linear temporal logic symbolic model checking ⋮ Backdoors for linear temporal logic ⋮ CTL update of Kripke models through protections ⋮ TABLEAUX: A general theorem prover for modal logics ⋮ Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic ⋮ A hierarchy of temporal logics with past ⋮ Axiomatising extended computation tree logic ⋮ Strategic reasoning with a bounded number of resources: the quest for tractability ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ A guide to completeness and complexity for modal logics of knowledge and belief ⋮ On the expressive power of hybrid branching-time logics ⋮ Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\) ⋮ Temporal Logic with Recursion. ⋮ One-pass Context-based Tableaux Systems for CTL and ECTL ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Rewrite rules for \(\mathrm{CTL}^\ast\) ⋮ A symbolic model for timed concurrent constraint programming ⋮ Model checking abilities of agents: a closer look ⋮ A purely model-theoretic proof of the exponential succinctness gap between CTL\(^{+}\) and CTL ⋮ Unnamed Item ⋮ \(\text{BTL}_{2}\) and the expressive power of \(\text{ECTL}^{+}\) ⋮ A Refined Resolution Calculus for CTL ⋮ From Philosophical to Industrial Logics ⋮ A clausal resolution method for CTL branching-time temporal logic ⋮ Cycle detection in computation tree logic ⋮ A Labeled Natural Deduction System for a Fragment of CTL * ⋮ A general tableau method for propositional interval temporal logics: theory and implementation ⋮ Branching time logics with multiagent temporal accessibility relations ⋮ Parameterized Complexity of CTL ⋮ From Monadic Logic to PSL ⋮ A novel approach to verifying context free properties of programs ⋮ Model checking for hybrid branching-time logics ⋮ Epistemic logic for rule-based agents ⋮ Reasoning about System-Degradation and Fault-Recovery with Deontic Logic ⋮ Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach ⋮ Temporal logic with recursion ⋮ Branching interval algebra: an almost complete picture ⋮ Branching-Time Temporal Logics with Minimal Model Quantifiers ⋮ The price of universality ⋮ An On-the-fly Tableau-based Decision Procedure for PDL-satisfiability ⋮ Completeness and Complexity of Multi-modal CTL ⋮ On the Complexity of Branching-Time Logics ⋮ Constructive Formalization of Hybrid Logic with Eventualities ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ Verifying time, memory and communication bounds in systems of reasoning agents ⋮ Multi-modal CTL: completeness, complexity, and an application ⋮ Tableaux and sequent calculi for \textsf{CTL} and \textsf{ECTL}: satisfiability test with certifying proofs and models ⋮ No easy puzzles: hardness results for jigsaw puzzles ⋮ A goal-directed decision procedure for hybrid PDL ⋮ Probabilistic Temporal Logics ⋮ Clausal resolution in a logic of rational agency ⋮ Proof-based verification approaches for dynamic properties: application to the information system domain

Cites Work

This page was built for publication: Decision procedures and expressiveness in the temporal logic of branching time