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.