Document Open Access Logo

Linear-Time Model Checking Branching Processes

Authors Stefan Kiefer, Pavel Semukhin, Cas Widdershoven

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.6.pdf
  • Filesize: 0.64 MB
  • 16 pages

Document Identifiers

Author Details

Stefan Kiefer
  • University of Oxford, UK
Pavel Semukhin
  • University of Oxford, UK
Cas Widdershoven
  • University of Oxford, UK

Funding

  • Kiefer, Stefan: supported by a Royal Society University Research Fellowship.

Cite As Get BibTex

Stefan Kiefer, Pavel Semukhin, and Cas Widdershoven. Linear-Time Model Checking Branching Processes. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CONCUR.2021.6

Abstract

(Multi-type) branching processes are a natural and well-studied model for generating random infinite trees. Branching processes feature both nondeterministic and probabilistic branching, generalizing both transition systems and Markov chains (but not generally Markov decision processes). We study the complexity of model checking branching processes against linear-time omega-regular specifications: is it the case almost surely that every branch of a tree randomly generated by the branching process satisfies the omega-regular specification? The main result is that for LTL specifications this problem is in PSPACE, subsuming classical results for transition systems and Markov chains, respectively. The underlying general model-checking algorithm is based on the automata-theoretic approach, using unambiguous Büchi automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Verification by model checking
Keywords
  • model checking
  • Markov chains
  • branching processes
  • automata
  • computational complexity

Metrics

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

Related Versions

References

  1. K.B. Athreya and P.E. Ney. Branching Processes. Springer, 1972. Google Scholar
  2. C. Baier, S. Kiefer, J. Klein, S. Klüppelholz, D. Müller, and J. Worrell. Markov chains and unambiguous Büchi automata. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV), volume 9779 of LNCS, pages 23-42, 2016. Google Scholar
  3. A. Berman and R.J. Plemmons. Nonnegative matrices in the mathematical sciences. SIAM, 1994. Google Scholar
  4. A. Borodin. On relating time and space to size and depth. SIAM Journal of Computing, 6(4):733-744, 1977. URL: https://doi.org/10.1137/0206054.
  5. A. Borodin, J. von zur Gathen, and J.E. Hopcroft. Fast parallel matrix and GCD computations. Information and Control, 52(3):241-256, 1982. URL: https://doi.org/10.1016/S0019-9958(82)90766-5.
  6. D. Bustan, S. Rubin, and M.Y. Vardi. Verifying omega-regular properties of Markov chains. In Computer Aided Verification (CAV), volume 3114 of Lecture Notes in Computer Science, pages 189-201. Springer, 2004. Google Scholar
  7. S. Chakraborty and J.-P. Katoen. Parametric LTL on Markov chains. In 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science, volume 8705 of Lecture Notes in Computer Science, pages 207-221. Springer, 2014. Google Scholar
  8. T. Chen, K. Dräger, and S. Kiefer. Model checking stochastic branching processes. In Mathematical Foundations of Computer Science (MFCS), volume 7464 of Lecture Notes in Computer Science, pages 271-282. Springer, 2012. Google Scholar
  9. R. Cleaveland, S.P. Iyer, and M. Narasimha. Probabilistic temporal logics via the modal mu-calculus. Theoretical Computer Science, 342(2-3):316-350, 2005. Google Scholar
  10. C. Courcoubetis and M. Yannakakis. Verifying temporal properties of finite-state probabilistic programs. In Symposium on Foundations of Computer Science (FOCS), pages 338-345. IEEE Computer Society, 1988. Google Scholar
  11. C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. Journal of the ACM, 42(4):857-907, 1995. Google Scholar
  12. J.-M. Couvreur, N. Saheb, and G. Sutre. An optimal automata approach to LTL model checking of probabilistic systems. In International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), volume 2850 of Lecture Notes in Computer Science, pages 361-375. Springer, 2003. Google Scholar
  13. J. Esparza, A. Gaiser, and S. Kiefer. A strongly polynomial algorithm for criticality of branching processes and consistency of stochastic context-free grammars. Information Processing Letters, 113(10-11):381-385, 2013. Google Scholar
  14. K. Etessami, E. Martinov, A. Stewart, and M. Yannakakis. Reachability for branching concurrent stochastic games. In International Colloquium on Automata, Languages, and Programming (ICALP), volume 132 of LIPIcs, pages 115:1-115:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  15. K. Etessami, A. Stewart, and M. Yannakakis. A polynomial time algorithm for computing extinction probabilities of multitype branching processes. SIAM Journal of Computing, 46(5):1515-1553, 2017. Google Scholar
  16. K. Etessami, A. Stewart, and M. Yannakakis. Greatest fixed points of probabilistic min/max polynomial equations, and reachability for branching Markov decision processes. Information and Computation, 261:355-382, 2018. Google Scholar
  17. K. Etessami, A. Stewart, and M. Yannakakis. Polynomial time algorithms for branching Markov decision processes and probabilistic min(max) polynomial Bellman equations. Mathematics of Operations Research, 45(1):34-62, 2020. Google Scholar
  18. K. Etessami and M. Yannakakis. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. Journal of the ACM, 56(1):1:1-1:66, 2009. Google Scholar
  19. K. Etessami and M. Yannakakis. Model checking of recursive probabilistic systems. ACM Transactions on Computational Logic, 13(2):12:1-12:40, 2012. URL: https://doi.org/10.1145/2159531.2159534.
  20. T. Gogacz, H. Michalewski, M. Mio, and M. Skrzypczak. Measure properties of regular sets of trees. Information and Computation, 256:108-130, 2017. Google Scholar
  21. A. Gorlin and C.R. Ramakrishnan. Separable GPL: decidable model checking with more non-determinism. In International Conference on Concurrency Theory (CONCUR), volume 118 of LIPIcs, pages 36:1-36:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  22. P. Haccou, P. Jagers, and V.A. Vatutin. Branching Processes: Variation, Growth, and Extinction of Populations. Cambridge University Press, 2005. Google Scholar
  23. T.E. Harris. The Theory of Branching Processes. Springer, 1963. Google Scholar
  24. S. Kiefer, P. Semukhin, and C. Widdershoven. Linear-time model checking branching processes. Technical report, arxiv.org, 2021. Available at URL: https://arxiv.org/abs/2107.01687.
  25. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Principles of Programming Languages (POPL), pages 97-107. ACM Press, 1985. Google Scholar
  26. H. Michalewski and M. Mio. On the problem of computing the probability of regular sets of trees. In Foundation of Software Technology and Theoretical Computer Science (FSTTCS), volume 45 of LIPIcs, pages 489-502. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  27. D. Niwiński, M. Przybyłko, and M. Skrzypczak. Computing measures of weak-MSO definable sets of trees. In International Colloquium on Automata, Languages, and Programming (ICALP), volume 168 of LIPIcs, pages 136:1-136:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  28. C.M. Papadimitriou. Computational complexity. Addison-Wesley, 1994. Google Scholar
  29. N. Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods Computer Science, 3(3), 2007. URL: https://doi.org/10.2168/LMCS-3(3:5)2007.
  30. A. Rabinovich. Complementation of finitely ambiguous Büchi automata. In Developments in Language Theory (DLT), volume 11088 of Lecture Notes in Computer Science, pages 541-552. Springer, 2018. Google Scholar
  31. A.P Sistla and E.M. Clarke. The complexity of propositional linear temporal logics. Journal of the ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  32. A.P. Sistla, M.Y. Vardi, and P. Wolper. The complementation problem for Büchi automata with appplications to temporal logic. Theoretical Computer Science, 49:217-237, 1987. URL: https://doi.org/10.1016/0304-3975(87)90008-9.
  33. A. Stewart, K. Etessami, and M. Yannakakis. Upper bounds for Newton’s method on monotone polynomial systems, and P-time model checking of probabilistic one-counter automata. Journal of the ACM, 62(4):30:1-30:33, 2015. Google Scholar
  34. W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science (Vol. B): Formal Models and Semantics, chapter 4, pages 133-191. MIT Press, 1990. Google Scholar
  35. M.Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of the 26th Annual Symposium on Foundations of Computer Science (FOCS), pages 327-338. IEEE Computer Society, 1985. URL: https://doi.org/10.1109/SFCS.1985.12.
  36. M.Y. Vardi. Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In Formal Methods for Real-Time and Probabilistic Systems, pages 265-276. Springer, 1999. Google Scholar
  37. M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In 1st Symposium on Logic in Computer Science (LICS), pages 332-344. IEEE Computer Society Press, 1986. Google Scholar
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact