Model checking the full modal mu-calculus for infinite sequential processes

DOI10.1016/S0304-3975(99)00034-1zbMath0933.68063MaRDI QIDQ1960527

Bernhard Steffen, Olaf Burkart

Publication date: 12 January 2000

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

zbMATH Keywords

regular graphsmodel checkinginfinite-state systemspushdown processesmodal mu-calculuscontext-free processes

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items (8)

A Branching Time Variant of CaRet ⋮ Model-checking structured context-free languages ⋮ Model Checking Procedural Programs ⋮ Towards the hierarchical verification of reactive systems ⋮ Regular model checking: evolution and perspectives ⋮ Be lazy and don't care: faster CTL model checking for recursive state machines ⋮ Automatic verification of recursive procedures with one integer parameter. ⋮ A saturation method for the modal \(\mu \)-calculus over pushdown systems

Cites Work

• Results on the propositional \(\mu\)-calculus
• The theory of ends, pushdown automata, and second-order logic
• The modal mu-calculus alternation hierarchy is strict
• An improved algorithm for the evaluation of fixpoint expressions
• Decidability of Second-Order Theories and Automata on Infinite Trees
• On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking the full modal mu-calculus for infinite sequential processes