Model Checking Probabilistic Pushdown Automata

Javier Esparza; Antonin Kucera; Richard Mayr

doi:10.2168/LMCS-2(1:2)2006

Javier Esparza ; Antonin Kucera ; Richard Mayr - Model Checking Probabilistic Pushdown Automata

lmcs:2256 - Logical Methods in Computer Science, March 7, 2006, Volume 2, Issue 1 - https://doi.org/10.2168/LMCS-2(1:2)2006

Model Checking Probabilistic Pushdown AutomataArticle

Authors: Javier Esparza ; Antonin Kucera ; Richard Mayr

We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for PCTL and the subclass of stateless pPDA. Finally, we consider the class of omega-regular properties and show that both qualitative and quantitative model checking for pPDA is decidable.

https://doi.org/10.2168/LMCS-2(1:2)2006

Source: arXiv.org:cs/0508003

Volume: Volume 2, Issue 1

Secondary volumes: Selected Papers of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004)

Published on: March 7, 2006

Imported on: December 9, 2004

Keywords: Computer Science - Logic in Computer Science, D.2.4, F.1.1, G.3

Licence: arXiv.org - Assumed non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

68Q15 - Complexity classes (hierarchies, relations among complexity classes, etc.)

Sources:

[1] zbMATH Open.

Bibliographic References

26 Documents citing this article

Francesco Pontiggia;Ezio Bartocci;Michele Chiari, 2025, POPACheck: A Model Checker for Probabilistic Pushdown Automata, Lecture notes in computer science, pp. 105-121, 10.1007/978-3-031-98679-6_5, https://doi.org/10.1007/978-3-031-98679-6_5.

Nathalie Bertrand;Patricia Bouyer;Thomas Brihaye;Paulin Fournier;Pierre Vandenhove, 2025, Decisiveness for Countable MDPs and Insights for NPLCSs and POMDPs, ORBi UMONS, pp. 70-98, 10.1007/978-3-031-97439-7_3, https://orbi.umons.ac.be/handle/20.500.12907/53139.

Alessandro Abate;Mirco Giacobbe;Diptarko Roy, 2024, Stochastic Omega-Regular Verification and Control with Supermartingales, Lecture notes in computer science, pp. 395-419, 10.1007/978-3-031-65633-0_18, https://doi.org/10.1007/978-3-031-65633-0_18.

Alessandro Abate;Mirco Giacobbe;Diptarko Roy;Yannik Schnitzer, 2024, Model Checking and Strategy Synthesis with Abstractions and Certificates, Lecture notes in computer science, pp. 360-391, 10.1007/978-3-031-75775-4_16.

Antonín Kučera, 2024, The Satisfiability and Validity Problems for Probabilistic CTL, Lecture notes in computer science, pp. 9-18, 10.1007/978-3-031-72621-7_2.

Alain Finkel;Serge Haddad;Lina Ye, 2023, Introducing Divergence for Infinite Probabilistic Models, SPIRE - Sciences Po Institutional REpository, pp. 127-140, 10.1007/978-3-031-45286-4_10, https://hal.science/hal-04271224.

Haihui Wang;Luyao Zhao;Yongxia He;Zhimin Han;Ping Li, 2023, Fuzzy pushdown automata based on complete residuated lattices: variants and computing powers, Soft Computing, 27, 11, pp. 6927-6938, 10.1007/s00500-023-08062-7.

Tobias Winkler;Joost-Pieter Katoen, 2023, Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, Lecture notes in computer science, pp. 391-409, 10.1007/978-3-031-30820-8_24, https://doi.org/10.1007/978-3-031-30820-8_24.

Miroslav Chodil;Antonín Kučera;Jan Křetínský, 2022, Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge, Lecture notes in computer science, pp. 364-387, 10.1007/978-3-031-22337-2_18.

Tobias Winkler;Christina Gehnen;Joost-Pieter Katoen, 2022, Model Checking Temporal Properties of Recursive Probabilistic Programs, Lecture notes in computer science, pp. 449-469, 10.1007/978-3-030-99253-8_23, https://doi.org/10.1007/978-3-030-99253-8_23.

Miroslav Chodil;Antonín Kučera, 2021, The Satisfiability Problem for a Quantitative Fragment of PCTL, Lecture notes in computer science, pp. 149-161, 10.1007/978-3-030-86593-1_10.

Mingzhang Huang;Hongfei Fu;Joost-Pieter Katoen, 2019, Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems, Information and Computation, 268, pp. 104431, 10.1016/j.ic.2019.05.004.

Tomáš Brázdil;Krishnendu Chatterjee;Antonín Kučera;Petr Novotný;Dominik Velan, 2019, Deciding Fast Termination for Probabilistic VASS with Nondeterminism, arXiv (Cornell University), pp. 462-478, 10.1007/978-3-030-31784-3_27, http://arxiv.org/abs/1907.11010.

Benjamin Lucien Kaminski;Joost-Pieter Katoen;Christoph Matheja;Federico Olmedo, 2018, Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms, Universidad de Chile, 65, 5, pp. 1-68, 10.1145/3208102, https://repositorio.uchile.cl/handle/2250/169551.

ANDREY GORLIN;C. R. RAMAKRISHNAN;SCOTT A. SMOLKA, 2012, Model checking with probabilistic tabled logic programming, Theory and Practice of Logic Programming, 12, 4-5, pp. 681-700, 10.1017/s1471068412000245.

Daniel Deutch, 2012, Querying Probabilistic Business Processes for Sub-Flows, Theory of Computing Systems, 52, 3, pp. 367-402, 10.1007/s00224-012-9391-6.

Daniel Deutch;Tova Milo, 2012, Business Processes: A Database Perspective, Synthesis lectures on data management, 4, 5, pp. 1-103, 10.2200/s00430ed1v01y201206dtm027.

Stefan Kiefer;Andrzej S. Murawski;Joël Ouaknine;Björn Wachter;James Worrell, 2012, On the Complexity of the Equivalence Problem for Probabilistic Automata, Lecture notes in computer science, pp. 467-481, 10.1007/978-3-642-28729-9_31, https://doi.org/10.1007/978-3-642-28729-9_31.

Daniel Deutch, 2011, Querying probabilistic business processes for sub-flows, Proceedings of the 14th International Conference on Database Theory, pp. 54-65, 10.1145/1938551.1938562.

Daniel Deutch;Tova Milo, 2011, A quest for beauty and wealth (or, business processes for database researchers), Proceedings of the thirtieth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, pp. 1-12, 10.1145/1989284.1989286.

Christel Baier;Boudewijn R. Haverkort;Holger Hermanns;Joost-Pieter Katoen, 2010, Performance evaluation and model checking join forces, University of Twente Research Information, 53, 9, pp. 76-85, 10.1145/1810891.1810912, https://research.utwente.nl/en/publications/6567d0fe-c782-4f9c-8978-eb2a36587e7c.

Javier Esparza;Stefan Kiefer;Michael Luttenberger, 2008, Derivation Tree Analysis for Accelerated Fixed-Point Computation, Lecture notes in computer science, pp. 301-313, 10.1007/978-3-540-85780-8_24.

Joost-Pieter Katoen, 2008, Perspectives in Probabilistic Verification, University of Twente Research Information, pp. 3-10, 10.1109/tase.2008.44, https://research.utwente.nl/en/publications/046770c1-1d8b-4801-9398-7cd36a7a9d12.

Nathalie Bertrand;Patricia Bouyer;Thomas Brihaye;Nicolas Markey, 2008, Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics, pp. 55-64, 10.1109/qest.2008.19.

Tomas Brazdil;Vojtech Forejt;Jan Kretinsky;Anton´ın Kucera, 2008, The Satisfiability Problem for Probabilistic CTL, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp. 391-402, 10.1109/lics.2008.21.

Bjorn Wachter;Lijun Zhang;Holger Hermanns, 2007, Probabilistic Model Checking Modulo Theories, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), 2, pp. 129-140, 10.1109/qest.2007.10.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3536 times.

This article's PDF has been downloaded 827 times.