Notes:
The original publication is available at link.springer.com.
|
Abstract.
We consider a class of infinite-state Markov decision processes
generated by stateless pushdown automata. This class corresponds to 1½-player games over graphs generated by BPA systems or (equivalently) 1-exit
recursive state machines. An extended reachability objective is specified by
two sets S and T of safe and terminal stack configurations, where the
membership to S and T depends just on the top-of-the-stack symbol. The
question is whether there is a suitable strategy such that the probability of
hitting a terminal configuration by a path leading only through safe configurations is equal to (or different from) a given x∈{0,1}. We show that the
qualitative extended reachability problem is decidable in polynomial time,
and that the set of all configurations for which there is a winning strategy
is effectively regular. More precisely, this set can be represented by a deterministic finite-state automaton with a fixed number of control states. This
result is a generalization of a recent theorem by Etessami & Yannakakis
which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our 1½-player BPA games) is decidable in polynomial
time. Interestingly, the properties of winning strategies for the extended
reachability objectives are quite different from the ones for termination,
and new observations are needed to obtain the result. As an application,
we derive the EXPTIME-completeness of the model-checking problem for
1½-player BPA games and qualitative PCTL formulae.
|