2026-07-22T10:50:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9639 2024-03-06T10:44:36Z ddc:004 open_access

Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems Hague, Matthew Meyer, Roland Muskalla, Sebastian Zimmermann, Martin Parity Games Safety Games Pushdown Systems Collapsible Pushdown Systems Higher-Order Recursion Schemes Model Checking We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in safety checking to be used for more expressive specifications. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matthew Hague and Roland Meyer and Sebastian Muskalla and Martin Zimmermann 2018 Is Part Of LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2018.57 urn:nbn:de:0030-drops-96396 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.57 eng https://creativecommons.org/licenses/by/3.0/legalcode