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

DOI10.1016/S0304-3975(99)00034-1MaRDI QIDQ1960527zbMATH OpenFDO

Authors Olaf Burkart, Bernhard Steffen

Publication date 12 January 2000

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

zbMATH Keywords

model checkingregular graphsinfinite-state systemsmodal mu-calculuscontext-free processespushdown processes

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Model checking the full modal mu-calculus for infinite sequential processes
• Pushdown processes: Games and model-checking
• Enriched μ–Calculus Pushdown Module Checking
• A saturation method for the modal \(\mu \)-calculus over pushdown systems
• scientific article; zbMATH DE number 751138

Cites work

• scientific article; zbMATH DE number 1231556 (Why is no real title available?)
• scientific article; zbMATH DE number 1231559 (Why is no real title available?)
• scientific article; zbMATH DE number 1232239 (Why is no real title available?)
• scientific article; zbMATH DE number 1142315 (Why is no real title available?)
• scientific article; zbMATH DE number 751138 (Why is no real title available?)
• scientific article; zbMATH DE number 2102748 (Why is no real title available?)
• scientific article; zbMATH DE number 794257 (Why is no real title available?)
• scientific article; zbMATH DE number 1456956 (Why is no real title available?)
• 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
• Results on the propositional \(\mu\)-calculus
• The modal mu-calculus alternation hierarchy is strict
• The theory of ends, pushdown automata, and second-order logic

Cited in

(12)

• Model-checking structured context-free languages
• A saturation method for the modal \(\mu \)-calculus over pushdown systems
• Formal Methods for Components and Objects
• Automatic verification of recursive procedures with one integer parameter.
• Be lazy and don't care: faster CTL model checking for recursive state machines
• Model checking procedural programs
• Towards the hierarchical verification of reactive systems
• Model checking the full modal mu-calculus for infinite sequential processes
• A Branching Time Variant of CaRet
• Regular model checking: evolution and perspectives
• scientific article; zbMATH DE number 4131643 (Why is no real title available?)
• Model-checking the higher-dimensional modal \(\mu\)-calculus

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

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