A saturation method for the modal \(\mu \)-calculus over pushdown systems

DOI10.1016/j.ic.2010.12.004zbMath1215.68151OpenAlexW2079590852MaRDI QIDQ532393

Yong-Cai Geng, Sumit K. Garg

Publication date: 4 May 2011

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2010.12.004

zbMATH Keywords

parity gamespushdown systemsglobal model checkingmodal \(\mu \)-calculussaturation methodswinning regions

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Combinatory logic and lambda calculus (03B40)

Related Items

Model Checking Procedural Programs ⋮ Be lazy and don't care: faster CTL model checking for recursive state machines ⋮ Efficient CTL model-checking for pushdown systems ⋮ A saturation method for the modal \(\mu \)-calculus over pushdown systems

Uses Software

• SLAM
• Bebop

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A saturation method for the modal \(\mu \)-calculus over pushdown systems
• Note on winning positions on pushdown games with \(\omega\)-regular conditions
• Model checking the full modal mu-calculus for infinite sequential processes
• Weighted pushdown systems and their application to interprocedural dataflow analysis
• Winning Regions of Pushdown Parity Games: A Saturation Method
• Computer Aided Verification
• A fixpoint calculus for local and global program flows
• Verification, Model Checking, and Abstract Interpretation
• Rudiments of \(\mu\)-calculus
• Reachability analysis of pushdown automata: Application to model-checking