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

Author Patricia Bouyer



PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.2.pdf
  • Filesize: 380 kB
  • 2 pages

Document Identifiers

Author Details

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

Acknowledgements

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

Cite As Get BibTex

Patricia Bouyer. On the Probabilistic and Statistical Verification of Infinite Markov Chains (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.2

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 [Abdulla et al., 2007], 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 [Younes and Simmons, 2006; H. L. S. Younes et al., 2010]. 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 [Kahn and Harris, 1951] 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 biase the original chain, and to estimate the probabilities in the biased chain; guarantees can sometimes be given, as studied for instance in [B. Barbot et al., 2012].
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 [P. Ballarini et al., 2015], and we discuss the methodology for experiments as well as our (partial) conclusions.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Markov processes
  • Theory of computation → Concurrency
Keywords
  • Markov Chains
  • Infinite state systems
  • Numerical and statistical Vverification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. P. A. Abdulla, N. B. Henda, and R. Mayr. Decisive Markov chains. Logical Methods in Computer Science, 3(4), 2007. URL: https://doi.org/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. URL: https://doi.org/10.1016/j.peva.2015.04.003.
  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. Google Scholar
  4. B. Barbot, P. Bouyer, and S. Haddad. Beyond decisiveness of infinite Markov chains. CoRR arXiV, 2024. URL: https://doi.org/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. URL: https://doi.org/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. Google Scholar
  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. URL: https://doi.org/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. URL: https://doi.org/10.1016/J.IC.2006.05.002.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail