Reachability in recursive Markov decision processes.

*(English)*Zbl 1145.91011A class of infinite-state Markov decision processes generated by stateless pushdown automata is considered. This class corresponds to 1 1/2-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\) in \((0,1)\). It is shown 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 and Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our 1 1/2-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, the EXPTIME-completeness of the model-checking problem is obtained for 1 1/2-player BPA games and qualitative PCTL formulae.

Reviewer: Giacomo Bonanno (Davis)

##### Software:

PRISM
PDF
BibTeX
XML
Cite

\textit{T. Brázdil} et al., Inf. Comput. 206, No. 5, 520--537 (2008; Zbl 1145.91011)

Full Text:
DOI

##### References:

[1] | Baier, C.; Kwiatkowska, M., Model checking for a probabilistic branching time logic with fairness, Distributed computing, 11, 3, 125-155, (1998) |

[2] | Bianco, A.; de Alfaro, L., Model checking of probabalistic and nondeterministic systems, (), 499-513 · Zbl 1354.68167 |

[3] | Bouajjani, A.; Esparza, J.; Maler, O., Reachability analysis of pushdown automata: application to model checking, (), 135-150 |

[4] | Brázdil, T.; Kučera, A.; Stražovský, O., On the decidability of temporal properties of probabilistic pushdown automata, (), 145-157 · Zbl 1118.68520 |

[5] | Esparza, J.; Kučera, A.; Mayr, R., Model-checking probabilistic pushdown automata, (), 12-21 |

[6] | Esparza, J.; Kučera, A.; Schwoon, S., Model-checking LTL with regular valuations for pushdown systems, Information and computation, 1862, 355-376, (2003) · Zbl 1078.68081 |

[7] | Etessami, K.; Yannakakis, M., Recursive Markov decision processes and recursive stochastic games, (), 891-903 · Zbl 1085.68089 |

[8] | Etessami, K.; Yannakakis, M., Efficient qualitative analysis of classes of recursive Markov decision processes and simple stochastic games, (), 634-645 · Zbl 1136.90499 |

[9] | () |

[10] | Feller, W., An introduction to probability theory and its applications, vol. 1, (1968), Wiley · Zbl 0155.23101 |

[11] | Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal aspects of computing, 6, 512-535, (1994) · Zbl 0820.68113 |

[12] | A. Hinton, M. Kwiatkowska, G. Norman, D. Parker, PRISM a tool for automatic verification of probabilistic systems, in: Proceedings of TACAS 2006, Lecture Notes in Computer Science, vol. 3920, Springer, 2006, pp. 441-444. |

[13] | Puterman, M.L., Markov decision processes, (1994), Wiley · Zbl 0336.93047 |

[14] | Walukiewicz, I., Pushdown processes: games and model-checking, Information and computation, 1642, 234-263, (2001) · Zbl 1003.68072 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.