Symbolic model checking for -calculus requires exponential time

DOI10.1016/S0304-3975(00)00033-5zbMATH Open0944.68035OpenAlexW2063651327MaRDI QIDQ1575656FDOQ1575656

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

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

Cited In (4)

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

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)