Projects per year
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.
Original language | English |
---|---|
Title of host publication | International Symposium of Mathematical Foundations of Computer Science |
Pages | 1-15 |
Number of pages | 15 |
DOIs | |
Publication status | Published - 20 Aug 2018 |
Publication series
Name | Leibniz International Proceedings in Informatics (LIPIcs) |
---|---|
Volume | 117 |
Keywords
- Parity Games, Safety Games, Pushdown Systems, Collapsible Pushdown Systems, Higher-Order Recursion Schemes, Model Checking
Projects
- 1 Finished
-
Verification of Concurrent and Higher-Order Recursive Programs
Hague, M. (PI)
Eng & Phys Sci Res Council EPSRC
1/05/13 → 30/04/18
Project: Research