Symbolic model checking for \(\mu\)-calculus requires exponential time

DOI10.1016/S0304-3975(00)00033-5zbMath0944.68035OpenAlexW2063651327MaRDI QIDQ1575656

Alexander Rabinovich

Publication date: 21 August 2000

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

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

zbMATH Keywords

complexitymodel checkingMU-calculus

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Related Items (2)

A parametric analysis of the state-explosion problem in model checking ⋮ Is your model checker on time? On the complexity of model checking for timed modal logics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Symbolic model checking: \(10^{20}\) states and beyond
• Propositional dynamic logic of regular programs
• Complexity of equivalence problems for concurrent systems of finite agents
• Succinct representations of graphs
• Alternation
• An automata-theoretic approach to branching-time model checking

This page was built for publication: Symbolic model checking for \(\mu\)-calculus requires exponential time