On model checking for the \(\mu\)-calculus and its fragments

DOI10.1016/S0304-3975(00)00034-7zbMath0973.68120OpenAlexW1974206804MaRDI QIDQ5941205

Charanjit S. Jutla, E. Allen Emerson, A. P. Sistla

Publication date: 20 August 2001

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00034-7

zbMATH Keywords

calculus model checking temporal logic expressiveness tree automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Temporal logic (03B44)

Related Items (61)

μ-Bicomplete Categories and Parity Games ⋮ On the universal and existential fragments of the \(\mu\)-calculus ⋮ Memoryless determinacy of parity and mean payoff games: a simple proof ⋮ Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\) ⋮ Permissive strategies: from parity games to safety games ⋮ The mu-calculus and Model Checking ⋮ Fast and simple nested fixpoints ⋮ From Parity and Payoff Games to Linear Programming ⋮ When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus ⋮ Parity game reductions ⋮ Deciding Parity Games in Quasi-polynomial Time ⋮ Logic programming approach to automata-based decision procedures ⋮ A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games ⋮ Robust worst cases for parity games algorithms ⋮ Parameterized Algorithms for Parity Games ⋮ Program schemata vs. automata for decidability of program logics ⋮ A polynomial space construction of tree-like models for logics with local chains of modal connectives ⋮ A gap property of deterministic tree languages. ⋮ Solving parity games by a reduction to SAT ⋮ Improved complexity analysis of quasi-polynomial algorithms solving parity games ⋮ Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games ⋮ Unnamed Item ⋮ Fixpoint logics over hierarchical structures ⋮ Model checking in the modal \(\mu \)-calculus and generic solutions ⋮ Unnamed Item ⋮ The dag-width of directed graphs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Model checking games for the quantitative \(\mu \)-calculus ⋮ On logics with two variables ⋮ A superpolynomial lower bound for strategy iteration based on snare memorization ⋮ Unnamed Item ⋮ Local Model Checking in a Logic for True Concurrency ⋮ Unnamed Item ⋮ Canonical completeness of infinitary \(\mu \) ⋮ Games for the \(\mu\)-calculus ⋮ Solving parity games via priority promotion ⋮ Unnamed Item ⋮ Energy parity games ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Ambiguous classes in \(\mu\)-calculi hierarchies ⋮ On model checking for the \(\mu\)-calculus and its fragments ⋮ Strategy logic ⋮ A parametric analysis of the state-explosion problem in model checking ⋮ Three notes on the complexity of model checking fixpoint logic with chop ⋮ Incremental reasoning on monadic second-order logics with logic programming ⋮ Facets of Synthesis: Revisiting Church’s Problem ⋮ Quasipolynomial computation of nested fixpoints ⋮ Deterministic Graphical Games Revisited ⋮ Certifying proofs for SAT-based model checking ⋮ Extracting Winning Strategies in Update Games ⋮ Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time ⋮ The modal mu-calculus alternation hierarchy is strict ⋮ Switching Graphs ⋮ Reasoning about nondeterministic and concurrent actions: A process algebra approach ⋮ Alternating Context-Free Languages and Linear Time μ-Calculus with Sequential Composition ⋮ Recursive algorithm for parity games requires exponential time ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics ⋮ Reduced models for efficient CCS verification ⋮ Games with winning conditions of high Borel complexity

Cites Work

This page was built for publication: On model checking for the \(\mu\)-calculus and its fragments