BPA games

Olivier Serre, LIAFA

A BPA is a special case of pushdown process that only have one state. As for pushdown, we associate with a BPA a graph whose nodes are the set of configurations of the BPA (i.e. the words on the BPA's alphabet) and whose edges are induced by the rewriting rules. We first assume that the rewriting rules of the BPA only depend on the top symbol and we partition the nodes between two players and we color them depending on their top letter: this defines a two players parity game on an infinite graph that we call a local parity BPA game. We show that for such a game, the winning strategy only depends on the top stack symbol and therefore, deciding the winner is in $\mathcal{NP}\cap co-\mathcal{NP}$. Then we give an algorithm to decide the winner in a local parity BPA game in exponential time in the number of colors. For this, we use a Turing reduction to parity games on finite graphs. Then we consider a natural generalization of local BPA games: global BPA games.

For this, the set of configuration is partitioned into two regular languages and colored according to a partition of the set of configurations into regular languages. Moreover, rewriting rules do not only depend on the top symbol but also on the color of the configuration. We give an exponential reduction to local BPA game that leads to a DEXPTIME algorithm to decide the winner in a global parity BPA game. As a by product we show that the set of winning positions for a given player is regular. Finally, we show that deciding the winner in a global parity BPA game is a DEXPTIME-hard problem.