Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems

DOI10.4230/LIPICS.MFCS.2018.57OpenAlexW2964194240MaRDI QIDQ5005159

Roland Meyer, Matthew Hague, Martín G. Zimmermann, Sebastian Muskalla

Publication date: 4 August 2021

Full work available at URL: https://arxiv.org/abs/1805.02963

zbMATH Keywords

parity gamesmodel checkingpushdown systemssafety gamescollapsible pushdown systemshigher-order recursion schemes

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items (1)

Liveness in broadcast networks

Uses Software

• TravMC2
• ByMC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Iterated stack automata and complexity classes
• A ZDD-Based Efficient Higher-Order Model Checking Algorithm
• Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
• Proving Liveness of Parameterized Programs
• Permissive strategies: from parity games to safety games
• Deciding parity games in quasipolynomial time
• Collapsible Pushdown Automata and Recursion Schemes
• A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
• A type-directed abstraction refinement approach to higher-order model checking

This page was built for publication: Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems