Formats of Winning Strategies for Six Types of Pushdown Games

TL;DR

This paper investigates the types of pushdown automata that can implement winning strategies across six different classes of pushdown games, revealing when the strategy type matches the game arena type and when it does not.

Contribution

It provides a unified proof method for four cases where strategy implementation matches the game arena type and identifies two cases where this correspondence fails.

Findings

Strategies are implementable by the same pushdown machine type in four cases.

In two cases, the implementation strategy type differs from the game arena type.

Addresses an abstract criterion explaining the matching and mismatching cases.

Abstract

The solution of parity games over pushdown graphs (Walukiewicz '96) was the first step towards an effective theory of infinite-state games. It was shown that winning strategies for pushdown games can be implemented again as pushdown automata. We continue this study and investigate the connection between game presentations and winning strategies in altogether six cases of game arenas, among them realtime pushdown systems, visibly pushdown systems, and counter systems. In four cases we show by a uniform proof method that we obtain strategies implementable by the same type of pushdown machine as given in the game arena. We prove that for the two remaining cases this correspondence fails. In the conclusion we address the question of an abstract criterion that explains the results.