<figure><img src="image_1.png" /></figure>

HAL
open science

# On the Probabilistic and Statistical Verification of Infinite Markov Chains (Invited Talk)

Patricia Bouyer

► To cite this version:

Patricia Bouyer. On the Probabilistic and Statistical Verification of Infinite Markov Chains (Invited Talk). CSL'25, Feb 2025, Amsterdam (NETHERLANDS), Netherlands. 10.4230/LIPIcs.CSL.2025.2 . hal-05344311

HAL Id: hal-05344311

https://hal.science/hal-05344311v1

Submitted on 5 Nov 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On the probabilistic and statistical verification of infinite Markov chains

Patricia Bouyer

Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles,
91190 Gif-sur-Yvette, France

## Abstract

The verification of infinite-state Markov chains is a challenging problem, even when those chains are described by structured high-level models. In 2007, Abdulla et al introduced the concept of decisiveness [1], and showed that a natural approximation scheme could be applied to infinite Markov chains that are decisive. This was, up to our knowledge, the unique generic scheme that could be widely applied to (decisive) infinite Markov chains providing guarantees on the computed values (under some mild assumptions for effectiveness). On the other hand, statistical model-checking is a very efficient method that can be used for estimating probabilities in stochastic systems [8, 7]. We explain in this talk that decisiveness is also a key concept that allows to apply such statistical methods to infinite Markov chains.

While decisiveness is a crucial property, not all Markov chains are decisive, and it is therefore desirable to propose methods to analyze non-decisive Markov chains. Importance sampling [6] is a method which has been proposed to improve efficiency of statistical model-checking, in particular for estimating probabilities of rare events in stochastic systems. The idea is to bias the original chain, and to estimate the probabilities in the biased chain; guarantees can sometimes be given, as studied for instance in [5].

In this talk, we will explain how we use the importance sampling idea to turn a non-decisive Markov chain into a biased decisive Markov chain, in which we can estimate probabilities (with guarantees). We apply the general approach to a class of probabilistic pushdown automata. Our algorithms have been implemented in the tool Cosmos [2], and we discuss the methodology for experiments as well as our (partial) conclusions.

**2012 ACM Subject Classification** Mathematics of computing → Markov processes; Theory of computation → Concurrency

**Keywords and phrases** Markov Chains, Infinite state systems, Numerical and statistical Verification

**Digital Object Identifier** 10.4230/LIPIcs.CSL.2025.2

**Category** Invited talk

**Related Version** A preliminary work on this topic appeared in [3], whose extended version is [4].
**Full Version:** https://arxiv.org/abs/2409.18670

**Funding** This work has been partly supported by ANR projects MAVeriQ (ANR-20-CE25-0012) and BisoUS (ANR-22-CE48-0012).

**Acknowledgements** I am thankful to Benoît Barbot and Serge Haddad for introducing me to the world of statistical model-checking.

## References

1. P. A. Abdulla, N. B. Henda, and R. Mayr. Decisive Markov chains. *Logical Methods in Computer Science*, 3(4), 2007. doi:10.2168/LMCS-3(4:7)2007.

2. P. Ballarini, B. Barbot, M. Duflot, S. Haddad, and N. Pekergin. HASL: A new approach for performance evaluation and model checking from concepts to experimentation. *Performance Evaluation*, 90:53–77, 2015. doi:10.1016/j.peva.2015.04.003.

<figure><img src="image_3.png" /></figure>
## 2:2 On the probabilistic and statistical verification of infinite Markov chains

3. B. Barbot, P. Bouyer, and S. Haddad. Beyond decisiveness of infinite Markov chains. In Proc. 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'24), volume 323 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1-8:21, 2024.

4. B. Barbot, P. Bouyer, and S. Haddad. Beyond decisiveness of infinite Markov chains. CoRR arXiv, 2024. doi:10.48550/arXiv.2409.18670.

5. B. Barbot, S. Haddad, and C. Picaronny. Coupling and importance sampling for statistical model checking. In 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214 of LNCS, pages 331-346. Springer, 2012. doi:10.1007/978-3-642-28756-5_23.

6. H. Kahn and T. E. Harris. Estimation of particle transmission by random sampling. National Bureau of Standards applied mathematics series, 12:27-30, 1951.

7. H. L. S. Younes, E. M. Clarke, and P. Zuliani. Statistical verification of probabilistic properties with unbounded until. In 13th Brazilian Symposium on Formal Methods (SBMF'10), volume 6527 of LNCS, pages 144-160. Springer, 2010. doi:10.1007/978-3-642-19829-8_10.

8. H. L. S. Younes and R. G. Simmons. Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation, 204(9):1368-1409, 2006. doi: 10.1016/J.IC.2006.05.002.