Reachability in Games over Probabilistic Pushdown Automata
Pushdown automata (PDA) form a natural model for finitely presented systems with recursive function calls. Partitioning the configurations of a PDA into stochastic and two kinds of non-deterministic ones allows to induce an infinite-state stochastic game. The evolution of systems modelled in this setting is driven by a controller and influenced by both a random "Nature" and a non-deterministic "evil environment". The play in these games is turn-based and has infinite duration.
We are interested in basic model-checking questions based on linear properties, mainly on reachability. A typical question is: "Is there a strategy for the controller such that under every response of the environment the probability of avoiding an error state is at least p?". A special case of these questions is the qualitative case, where the probability constraint ("p" in the previous example) is restricted to be 0 or 1.
Since already answering some qualitative reachability questions is undecidable for PDA games, even if there is no evil environment involved, the tradeoff between expressibility and decidability is very important here. In particular, restricting to the following natural subclasses of PDA yields interesting results: BPA (PDA without control states), and one-counter machines (OC). These subclasses still contain finite games as a proper subset. Several decidability results will be presented for model-checking in these subclasses. The talk is based on several joint works with T. Brázdil, K. Etessami, V. Forejt, A. Kučera, J. Obdržálek and D. Wojtczak.