Decisiveness for Countable MDPs and Insights for NPLCSs and POMDPs

[en] Markov chains and Markov decision processes (MDPs) are well-established probabilistic models. While finite Markov models are well-understood, analyzing their infinite counterparts remains a significant challenge. Decisiveness has proven to be an elegant property for countable Markov chains: it is general enough to be satisfied by several natural classes of countable Markov chains, and it is a sufficient condition for simple qualitative and approximate quantitative model-checking algorithms to exist. In contrast, existing works on the formal analysis of countable MDPs usually rely on ad hoc techniques tailored to specific classes. We provide here a general framework to analyze countable MDPs by extending the notion of decisiveness. Compared to Markov chains, MDPs exhibit extra non-determinism that can be resolved in an adversarial or cooperative way, leading to multiple natural notions of decisiveness. We show that these notions enable the approximation of reachability and safety probabilities in countable MDPs using simple model-checking procedures. We then instantiate our generic approach to two concrete classes of models inducing countable MDPs: non-deterministic probabilistic lossy channel systems and partially observable MDPs. This leads to an algorithm to approximately compute safety probabilities in each of these classes.

Research center :

CREMMI - Modélisation mathématique et informatique

Disciplines :

Computer science
Mathematics

Author, co-author :

Bertrand, Nathalie ; INRIA - Institut National de Recherche en Informatique et en Automatique > Rennes

Bouyer, Patricia ; Université Paris-Saclay, CNRS > Laboratoire Méthodes Formelles (LMF)

BRIHAYE, Thomas ; Université de Mons - UMONS > Faculté des Sciences > Service de Mathématiques effectives

Fournier, Paulin

VANDENHOVE, Pierre ; Université de Mons - UMONS > Faculté des Sciences > Service d'Informatique théorique

Language :

English

Title :

Decisiveness for Countable MDPs and Insights for NPLCSs and POMDPs

Publication date :

30 August 2025

Event name :

Principles of Formal Quantitative Analysis

Event organizer :

Bertrand, N., Dubslaff, C., Klüppelholz, S.

Event place :

Aarhus, Denmark

Event date :

30 August 2025

By request :

Yes

Audience :

International

Main work title :

Lecture Notes in Computer Science

Publisher :

Springer Nature Switzerland

ISBN/EAN :

978-3-03-197439-7
978-3-03-197438-0

Pages :

70–98

Peer review/Selection committee :

Editorial reviewed

Additional URL :

https://link.springer.com/content/pdf/10.1007/978-3-031-97439-7_3

Research unit :

S829 - Informatique théorique
S820 - Mathématiques effectives

Research institute :

Complexys
Infortech

Funders :

F.R.S.-FNRS - Fonds de la Recherche Scientifique

Funding number :

T.0027.21

Funding text :

Thomas Brihaye is partly supported by the Fonds de la Recherche Scientiﬁque - FNRS under grant n◦ T.0027.21 and by the Belgian National Lottery.

Available on ORBi UMONS :

since 03 September 2025

Statistics

Number of views

31 (2 by UMONS)

Number of downloads

47 (3 by UMONS)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

Bibliography

Abdulla, P.A., Ben Henda, N., Mayr, R.: Decisive Markov chains. Logical Methods Comput. Sci. 3(4:7), 1–32 (2007). https://doi.org/10.2168/LMCS-3(4:7)2007
Abdulla, P.A., Bertrand, N., Rabinovich, A., Schnoebelen, P.: Verification of prob-abilistic systems with faulty communication. Inf. Comput. 202(2), 141–165 (2005). https://doi.org/10.1016/J.IC.2005.05.008
Abdulla, P.A., Clemente, L., Mayr, R., Sandberg, S.: Stochastic parity games on lossy channel systems. Logical Methods Comput. Sci. 10(4) (2014). https://doi.org/10.2168/LMCS-10(4:21)2014
de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stan-ford University, Stanford, CA (1997). http://i.stanford.edu/pub/cstr/reports/cs/tr/98/1601/CS-TR-98-1601.pdf
Baier, C., Bertrand, N., Schnoebelen, P.: A note on the attractor-property of infinite-state Markov chains. Inf. Process. Lett. 97(2), 58–63 (2006). https://doi.org/10.1016/j.ipl.2005.09.011
Baier, C., Bertrand, N., Schnoebelen, Ph.: Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Trans. Comput. Logic 9(1) (2007). https://doi.org/10.1145/1297658.1297663
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)
Barbot, B., Bouyer, P., Haddad, S.: Beyond decisiveness of infinite Markov chains. In: Proceedings of 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). LIPIcs, vol. 323, pp. 8:1–8:22. Leibniz-Zentrum für Informatik (2024). https://doi.org/10.4230/LIPIcs.FSTTCS.2024.8
Bertrand, N., Bouyer, P., Brihaye, T., Fournier, P., Vandenhove, P.: Deci-siveness for countable MDPs and insights for NPLCSs and POMDPs. CoRR abs/2008.10426 (2020). https://arxiv.org/abs/2008.10426
Bertrand, N., Schnoebelen, P.: Model checking lossy channels systems is probably decidable. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 120–135. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36576-18
Bertrand, N., Schnoebelen, Ph.: Solving stochastic B¨uchi games on infinite arenas with a finite attractor. In: Proceedings of 11th International Workshop on Quan-titative Aspects of Programming Languages and Systems (QAPL 2013). EPTCS, vol. 117, pp. 116–131 (2013). https://doi.org/10.4204/EPTCS.117.8
Brázdil, T., Brozek, V., Etessami, K.: One-counter stochastic games. In: Pro-ceedings IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’10). LIPIcs, vol. 8, pp. 108–119. Leibniz-Zentrum für Informatik (2010). https://doi.org/10.4230/LIPIcs.FSTTCS.2010.108
Brázdil, T., Brožek, V., Etessami, K., Kučera, A.: Approximating the termination value of one-counter MDPs and stochastic games. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 332–343. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22012-826
Brázdil, T., Brozek, V., Kucera, A., Obdrzálek, J.: Qualitative reachability in stochastic BPA games. Inf. Comput. 209(8), 1160–1183 (2011). https://doi.org/10.1016/J.IC.2011.02.002
Brázdil, T., et al.: Verification of Markov decision processes using learning algo-rithms. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 98– 114. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11936-6 8
Chatterjee, K., Chmelik, M., Tracol, M.: What is decidable about partially observ-able Markov decision processes with ω-regular objectives. J. Comput. Syst. Sci. 82(5), 878–911 (2016). https://doi.org/10.1016/J.JCSS.2016.02.009
Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203–224 (1992). https://doi.org/10.1016/0890-5401(92)90048-K
Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern prob-abilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9 31
Etessami, K., Wojtczak, D., Yannakakis, M.: Quasi-birth-death processes, tree-like QBDs, probabilistic 1-counter automata, and pushdown systems. Perform. Eval. 67(9), 837–857 (2010). https://doi.org/10.1016/j.peva.2009.12.009
Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. Logical Methods Comput. Sci. 4(4) (2008). https://doi.org/10.2168/LMCS-4(4:7)2008
Fijalkow, N.: Undecidability results for probabilistic automata. ACM SIGLOG News 4(4), 10–17 (2017). https://doi.org/10.1145/3157831.3157833
Finkel, A., Haddad, S., Ye, L.: About decisiveness of dynamic probabilistic models. In: Proceedings of 34th International Conference on Concurrency Theory (CON-CUR’23). LIPIcs, vol. 279, pp. 14:1–14:17. Leibniz-Zentrum f¨ur Informatik (2023). https://doi.org/10.4230/LIPICS.CONCUR.2023.14
Gimbert, H., Oualhadj, Y.: Probabilistic automata on finite words: decidable and undecidable problems. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 527–538. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14162-144
Haddad, S., Monmege, B.: Interval iteration algorithm for MDPs and IMDPs. Theoret. Comput. Sci. 735, 111–131 (2018). https://doi.org/10.1016/j.tcs.2016.12.003
Iyer, S., Narasimha, M.: Probabilistic lossy channel systems. In: Proceedings 7th International Conference on Theory and Practice of Software Development (TAP-SOFT’97). Lecture Notes in Computer Science, vol. 1214, pp. 667–681. Springer, Cham (1997). https://doi.org/10.1007/BFB0030633
Kaelbling, L., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1–2), 99–134 (1998). https://doi.org/10.1016/S0004-3702(98)00023-X
Kiefer, S., Mayr, R., Shirmohammadi, M., Totzke, P., Wojtczak, D.: How to play in infinite MDPs (invited talk). In: Czumaj, A., Dawar, A., Merelli, E. (eds.) Proc. 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). LIPIcs, vol. 168, pp. 3:1–3:18. Leibniz-Zentrum f¨ur Informatik (2020). https://doi.org/10.4230/LIPICS.ICALP.2020.3
Kiefer, S., Mayr, R., Shirmohammadi, M., Wojtczak, D.: Parity objectives in count-able MDPs. In: Proceedings of 32th Annual Symposium on Logic in Computer Science (LICS 2017), pp. 1–11. IEEE Computer Society Press (2017). https://doi.org/10.1109/LICS.2017.8005100
Kucera, A.: Lectures in Game Theory for Computer Scientists. Cambridge Univer-sity Press, Turn-Based Stochastic Games (2011). chap
Kucera, A., Esparza, J., Mayr, R.: Model checking probabilistic pushdown automata. Logical Methods Comput. Sci. 2(1) (2006). https://doi.org/10.2168/LMCS-2(1:2)2006
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-147
Madani, O., Hanks, S., Condon, A.: On the undecidability of probabilistic planning and infinite-horizon partially observable Markov decision problems. In: Hendler, J., Subramanian, D. (eds.) Proc. 16th National Conference on Artificial Intelligence and Eleventh Conference on Innovative Applications of Artificial Intelligence, pp. 541–548. AAAI Press/The MIT Press (1999)
Ornstein, D.: On the existence of stationary optimal strategies. Proc. Am. Math. Soc. 20(2), 563–569 (1969). http://www.jstor.org/stable/2035700
Paz, A.: Introduction to Probabilistic Automata. Academic Press (1971)
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Pro-gramming. Wiley Series in Probability and Statistics, Wiley, 1st edn. (1994). https://doi.org/10.1002/9780470316887
Sericola, B.: Markov Chains: Theory, Algorithms and Applications. Wiley, Hoboken (2013)
Shapley, L.S.: Stochastic games. Proc. Natl. Acad. Sci. 39(10), 1095–1100 (1953). https://doi.org/10.1073/pnas.39.10.1095