LIPIcs.FSTTCS.2024.8.pdf
- Filesize: 0.99 MB
- 22 pages
Document
Beyond Decisiveness of Infinite Markov Chains
Authors
Benoît Barbot 
,
Patricia Bouyer ,
Serge Haddad
-
Part of:
Volume:
44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-12-05
File
Document Identifiers
Author Details
- Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, 91190 Gif-sur-Yvette, France
Cite As Get BibTex
Benoît Barbot, Patricia Bouyer, and Serge Haddad. Beyond Decisiveness of Infinite Markov Chains. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSTTCS.2024.8
Abstract
Verification of infinite-state Markov chains is still a challenge despite several fruitful numerical or statistical approaches. For decisive Markov chains, there is a simple numerical algorithm that frames the reachability probability as accurately as required (however with an unknown complexity). On the other hand when applicable, statistical model checking is in most of the cases very efficient. Here we study the relation between these two approaches showing first that decisiveness is a necessary and sufficient condition for almost sure termination of statistical model checking. Afterwards we develop an approach with application to both methods that substitutes to a non decisive Markov chain a decisive Markov chain with the same reachability probability. This approach combines two key ingredients: abstraction and importance sampling (a technique that was formerly used for efficiency). We develop this approach on a generic formalism called layered Markov chain (LMC). Afterwards we perform an empirical study on probabilistic pushdown automata (an instance of LMC) to understand the complexity factors of the statistical and numerical algorithms. To the best of our knowledge, this prototype is the first implementation of the deterministic algorithm for decisive Markov chains and required us to solve several qualitative and numerical issues.
Subject Classification
ACM Subject Classification
- Mathematics of computing → Markov processes
- Theory of computation → Concurrency
Keywords
- Markov Chains
- Infinite State Systems
- Numerical and Statistical Verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
Supplementary Materials
-
Software (Source Code)
https://git.lacl.fr/barbot/Cosmos
browse
archived version
References
- 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.
- 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.
- 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.
- 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.
- J. Esparza, A. Kucera, and R. Mayr. Model Checking Probabilistic Pushdown Automata. Logical Methods in Computer Science, 2(1), 2006. URL: https://doi.org/10.2168/LMCS-2(1:2)2006.
-
G. Fayolle, V.A. Malyshev, and M. V. Menshikov. Topics in the Constructive Theory of Countable Markov Chains. Cambridge University Press, 1995.
- A. Finkel, S. Haddad, and L. Ye. About decisiveness of dynamic probabilistic models. In 34th International Conference on Concurrency Theory (CONCUR'23), volume 279 of LIPIcs, pages 14:1-14:17. Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CONCUR.2023.14.
- A. Finkel, S. Haddad, and L. Ye. Introducing divergence for infinite probabilistic models. In 17th International Conference on Reachability Problems (RP'23), volume 14235 of LNCS, pages 1-14. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-45286-4_10.
- F. G. Foster. On the Stochastic Matrices Associated with Certain Queuing Processes. The Annals of Mathematical Statistics, 24(3):355-360, 1953. URL: https://doi.org/10.1214/aoms/1177728976.
-
W. Hoeffding. Probability inequalities for sums of bounded random variables. J. Amer. Statist. Assoc., 58:13-30, 1963.
- W. Kahan. Pracniques: further remarks on reducing truncation errors. Comm. ACM, 8(1):40, 1965. URL: https://doi.org/10.1145/363707.363723.
-
H. Kahn and T. E. Harris. Estimation of particle transmission by random sampling. National Bureau of Standards applied mathematics series, 12:27-30, 1951.
- G. Rubino and B. Tuffin, editors. Rare Event Simulation using Monte Carlo Methods. Wiley, 2009. URL: https://doi.org/10.1002/9780470745403.
- J. M. Rutten, M. Z. Kwiatkowska, G. Norman, D. Parker, and P. Panangaden. Mathematical techniques for analyzing concurrent and probabilistic systems, volume 23 of CRM monograph series. American Mathematical Society, 2004. URL: http://www.ams.org/publications/authors/books/postpub/crmm-23.
- 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.
- 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.
- H. L. S. Younes and R. G. Simmons. Probabilistic verification of discrete event systems using acceptance sampling. In 14th International Conference on Computer-Aided Verification (CAV'02), volume 2404 of LNCS, pages 223-235. Springer, 2022. URL: https://doi.org/10.1007/3-540-45657-0_17.