An automata theoretic decision procedure for the propositional mu- calculus

DOI10.1016/0890-5401(89)90031-XzbMath0671.03023OpenAlexW2083398633MaRDI QIDQ1119630

Publication date: 1989

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(89)90031-x

zbMATH Keywords

tree automata elementary complexity propositional dynamic logic propositional mu-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25) General topics in the theory of software (68N01)

Related Items (55)

CTL$^*$ and ECTL$^*$ as fragments of the modal $\mu$-calculus ⋮ Abstraction in Fixpoint Logic ⋮ Is there a ``Hilbert thesis? ⋮ The mu-calculus and Model Checking ⋮ Compositional verification of concurrent systems by combining bisimulations ⋮ Two Ways to Common Knowledge ⋮ Logic programming approach to automata-based decision procedures ⋮ Proving properties of dynamic process networks ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Deciding the unguarded modal -calculus ⋮ Axiomatising extended computation tree logic ⋮ Fixed point characterization of infinite behavior of finite-state systems ⋮ Program schemata vs. automata for decidability of program logics ⋮ A survey on satisfiability checking for the $\mu $-calculus through tree automata ⋮ Unnamed Item ⋮ A tableau proof system for a mazurkiewicz trace logic with fixpoints ⋮ Unnamed Item ⋮ Mathematical modal logic: A view of its evolution ⋮ Bisimulation-invariant PTIME and higher-dimensional $\mu$-calculus ⋮ Alternation-free weighted mu-calculus: decidability and completeness ⋮ A Note on the Completeness of Kozen's Axiomatisation of the Propositional μ-Calculus ⋮ Completions of $\mu $-algebras ⋮ Local Model Checking in a Logic for True Concurrency ⋮ The Proof Theory of Common Knowledge ⋮ Canonical completeness of infinitary $\mu $ ⋮ Games for the $\mu$-calculus ⋮ Axiomatising extended computation tree logic ⋮ Local model checking for infinite state spaces ⋮ The Modal μ-Calculus Caught Off Guard ⋮ Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics ⋮ The complexity of identifying characteristic formulae ⋮ Completeness for the modal $\mu$-calculus: separating the combinatorics from the dynamics ⋮ The modal mu-calculus alternation hierarchy is strict ⋮ A selection property of the boolean $\mu $-calculus and some of its applications ⋮ Answering regular path queries in expressive description logics via alternating tree-automata ⋮ Ambiguous classes in $\mu$-calculi hierarchies ⋮ On model checking for the $\mu$-calculus and its fragments ⋮ On modal $\mu$-calculus and non-well-founded set theory ⋮ A Note on Negative Tagging for Least Fixed-Point Formulae ⋮ Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski ⋮ On modal $\mu $-calculus and Gödel-Löb logic ⋮ Automata, Logic and Games for the $$\lambda $$ -Calculus ⋮ The modal mu-calculus alternation hierarchy is strict ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ The modalμ-calculus hierarchy over restricted classes of transition systems ⋮ From Parity Games to Circular Proofs ⋮ A decidable class of problems for control under partial observation ⋮ Completeness of Kozen's axiomatisation of the propositional $\mu$-calculus. ⋮ Combining deduction and model checking into tableaux and algorithms for converse-PDL. ⋮ Inductive synthesis of recursive processes from logical properties ⋮ Pushdown processes: Games and model-checking ⋮ Tarskian set constraints ⋮ Automated Synthesis of Enforcing Mechanisms for Security Properties in a Timed Setting ⋮ Bounded game-theoretic semantics for modal mu-calculus ⋮ Monadic second-order logic on tree-like structures

Cites Work

This page was built for publication: An automata theoretic decision procedure for the propositional mu- calculus