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

Published on: March 7, 2006

Submitted 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

20 Documents citing this article

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, Lecture notes in computer science, Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, pp. 391-409, 2023, 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ý, Lecture notes in computer science, Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge, pp. 364-387, 2022, 10.1007/978-3-031-22337-2_18.

Tobias Winkler;Christina Gehnen;Joost-Pieter Katoen, Lecture notes in computer science, Model Checking Temporal Properties of Recursive Probabilistic Programs, pp. 449-469, 2022, 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, arXiv (Cornell University), The Satisfiability Problem for a Quantitative Fragment of PCTL, pp. 149-161, 2021, 10.1007/978-3-030-86593-1_10, https://arxiv.org/abs/2107.03794.

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, https://doi.org/10.1016/j.ic.2019.05.004.

Tomáš Brázdil;Krishnendu Chatterjee;Antonín Kučera;Petr Novotný;Dominik Velan, arXiv (Cornell University), Deciding Fast Termination for Probabilistic VASS with Nondeterminism, pp. 462-478, 2019, 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, UCL Discovery (University College London), 65, 5, pp. 1-68, 10.1145/3208102, https://discovery.ucl.ac.uk/id/eprint/10089685/.

ANDREY GORLIN;C. R. RAMAKRISHNAN;SCOTT A. SMOLKA, 2012, Model checking with probabilistic tabled logic programming, arXiv (Cornell University), 12, 4-5, pp. 681-700, 10.1017/s1471068412000245, https://arxiv.org/abs/1204.4736.

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, Library Union Catalog of Bavaria, Berlin and Brandenburg (B3Kat Repository), 4, 5, pp. 1-103, 10.2200/s00430ed1v01y201206dtm027, https://doi.org/10.2200/S00430ED1V01Y201206DTM027.

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

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

Daniel Deutch;Tova Milo, CiteSeer X (The Pennsylvania State University), A quest for beauty and wealth (or, business processes for database researchers), 2011, Athens Greece, 10.1145/1989284.1989286, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.221.5453.

Christel Baier;Boudewijn R. Haverkort;Holger Hermanns;Joost-Pieter Katoen, 2010, Performance evaluation and model checking join forces, Communications of the ACM, 53, 9, pp. 76-85, 10.1145/1810891.1810912.

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

Joost-Pieter Katoen, Data Archiving and Networked Services (DANS), Perspectives in Probabilistic Verification, pp. 3-10, 2008, Nanjing, China, 10.1109/tase.2008.44, https://research.utwente.nl/en/publications/046770c1-1d8b-4801-9398-7cd36a7a9d12.

Nathalie Bertrand;Patricia Bouyer;Thomas Brihaye;Nicolas Markey, CiteSeer X (The Pennsylvania State University), Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics, pp. 55-64, 2008, St Malo, France, 10.1109/qest.2008.19, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.218.665.

Tomas Brazdil;Vojtech Forejt;Jan Kretinsky;Anton´ın Kucera, CiteSeer X (The Pennsylvania State University), The Satisfiability Problem for Probabilistic CTL, pp. 391-402, 2008, Pittsburgh, PA, 10.1109/lics.2008.21, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.178.6093.

Bjorn Wachter;Lijun Zhang;Holger Hermanns, Fourth International Conference on the Quantitative Evaluation of Systems (QEST 2007), Probabilistic Model Checking Modulo Theories, 2007, Edinburgh, Scotland, UK, 10.1109/qest.2007.10.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1800 times.

This article's PDF has been downloaded 597 times.