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

TL;DR

This paper presents a direct polynomial-time reduction from parity games to safety games over collapsible pushdown systems, enabling more efficient safety verification for complex computational models.

Contribution

It provides the first direct polynomial-time reduction for parity to safety games on collapsible pushdown systems, combining existing techniques with three new methods.

Findings

Established a polynomial-time reduction from parity to safety games

Enhanced safety checking techniques for collapsible pushdown systems

Contributed to the trend of liveness-to-safety reductions

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.