Document Open Access Logo

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

Authors Matthew Hague , Roland Meyer, Sebastian Muskalla , Martin Zimmermann

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2018.57.pdf
  • Filesize: 465 kB
  • 15 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Verification by model checking
  • Theory of computation → Grammars and context-free languages
Keywords
  • Parity Games
  • Safety Games
  • Pushdown Systems
  • Collapsible Pushdown Systems
  • Higher-Order Recursion Schemes
  • Model Checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 57:1-57:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.MFCS.2018.57

Author Details

Matthew Hague
  • Royal Holloway, University of London, UK
Roland Meyer
  • TU Braunschweig, Germany
Sebastian Muskalla
  • TU Braunschweig, Germany
Martin Zimmermann
  • Universität des Saarlandes, Saarbrücken, Germany

Funding

  • Hague, Matthew: Supported by the EPSRC under grant [EP/K009907/1].
  • Zimmermann, Martin: Supported by the DFG under grant [ZI 1516/1-1].

References

  1. J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to safety games. ITA, 2002. Google Scholar
  2. D. Berwanger and L. Doyen. On the Power of Imperfect Information. In FSTTCS, 2008. Google Scholar
  3. A. Biere, C. Artho, and V. Schuppan. Liveness checking as safety checking. Electr. Notes Theor. Comput. Sci., 2002. Google Scholar
  4. R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and J. Widder. Decidability in parameterized verification. SIGACT News, 47(2), 2016. Google Scholar
  5. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, 1997. Google Scholar
  6. C. H. Broadbent and N. Kobayashi. Saturation-based model checking of higher-order recursion schemes. In CSL, 2013. Google Scholar
  7. T. Cachat and I. Walukiewicz. The complexity of games on higher order pushdown automata. CoRR, abs/0705.0262, 2007. Google Scholar
  8. C. S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In STOC, 2017. Google Scholar
  9. A. Carayol, M. Hague, A. Meyer, C.-H. L. Ong, and O. Serre. Winning Regions of Higher-Order Pushdown Games. In LICS, 2008. Google Scholar
  10. J. Daniel, A. Cimatti, A. Griggio, S. Tonetta, and S. Mover. Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In CAV, 2016. Google Scholar
  11. J. Engelfriet. Iterated stack automata and complexity classes. Inf. Comput., 95(1):21-75, 1991. Google Scholar
  12. A. Farzan, Z. Kincaid, and A. Podelski. Proving liveness of parameterized programs. In LICS, 2016. Google Scholar
  13. J. Fearnley, S. Jain, S. Schewe, F. Stephan, and D. Wojtczak. An ordered approach to solving parity games in quasi polynomial time and quasi linear space. In SPIN, 2017. Google Scholar
  14. W. Fridman and M. Zimmermann. Playing pushdown parity games in a hurry. In GandALF, 2012. Google Scholar
  15. K. Fujima, S. Ito, and N. Kobayashi. Practical alternating parity tree automata model checking of higher-order recursion schemes. In APLAS, 2013. Google Scholar
  16. M. Hague, R. Meyer, S. Muskalla, and M. Zimmermann. Parity to safety in polynomial time for pushdown and collapsible pushdown systems. CoRR, abs/1805.02963, 2018. URL: http://arxiv.org/abs/1805.02963.
  17. M. Hague, A. S. Murawski, C.-H. Luke Ong, and O. Serre. Collapsible pushdown automata and recursion schemes. In LICS, 2008. Google Scholar
  18. M. Jurdzinski and R. Lazic. Succinct progress measures for solving parity games. In LICS, pages 1-9, 2017. Google Scholar
  19. T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS '02: Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, pages 205-222, London, UK, 2002. Springer-Verlag. Google Scholar
  20. N. Kobayashi. HorSat2: A model checker for HORS based on SATuration. A tool available at URL: http://www-kb.is.s.u-tokyo.ac.jp/~koba/horsat2/.
  21. I. V. Konnov, M. Lazic, H. Veith, and J. Widder. A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In POPL, 2017. Google Scholar
  22. G. Lenzi. The modal μ-calculus: a survey. Task quarterly, 9(3):293-316, 2005. Google Scholar
  23. R. P. Neatherway and C.-H. L. Ong. Travmc2: higher-order model checking for alternating parity tree automata. In SPIN, 2014. Google Scholar
  24. C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, 2006. Google Scholar
  25. O. Padon, J. Hoenicke, G. Losa, A. Podelski, M. Sagiv, and S. Shoham. Reducing liveness to safety in first-order logic. PACMPL, 2017. Google Scholar
  26. A. Podelski and A. Rybalchenko. Transition invariants. In LICS, 2004. Google Scholar
  27. A. Podelski and A. Rybalchenko. Transition invariants and transition predicate abstraction for program termination. In TACAS, 2011. Google Scholar
  28. S. J. Ramsay, R. P. Neatherway, and C.-H. L. Ong. A type-directed abstraction refinement approach to higher-order model checking. In POPL, 2014. Google Scholar
  29. V. Schuppan and A. Biere. Liveness checking as safety checking for infinite state spaces. Electr. Notes Theor. Comput. Sci., 2005. Google Scholar
  30. S. Sohail and F. Somenzi. Safety first: A two-stage algorithm for ltl games. In FMCAD, 2009. Google Scholar
  31. T. Terao and N. Kobayashi. A zdd-based efficient higher-order model checking algorithm. In APLAS, 2014. Google Scholar
  32. I. Walukiewicz. Pushdown processes: Games and model checking. In CAV, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact