Symbolic model checking for -calculus requires exponential time

DOI10.1016/S0304-3975(00)00033-5MaRDI QIDQ1575656zbMATH OpenOpenAlexFDO

Authors 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)

Cites work

• scientific article; zbMATH DE number 108434 (Why is no real title available?)
• scientific article; zbMATH DE number 1351076 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 3328173 (Why is no real title available?)
• Alternation
• An automata-theoretic approach to branching-time model checking
• Complexity of equivalence problems for concurrent systems of finite agents
• Propositional dynamic logic of regular programs
• Results on the propositional \(\mu\)-calculus
• Succinct representations of graphs
• Symbolic model checking: \(10^{20}\) states and beyond

Cited in

(4)

• A parametric analysis of the state-explosion problem in model checking
• Distributed symbolic model checking for \(\mu\)-calculus
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Some results on complexity of \(\mu\)-calculus evaluation in the black-box model

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1575656)