2026-07-29T10:45:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14383 2024-03-06T10:54:16Z ddc:004 open_access

Linear-Time Model Checking Branching Processes Kiefer, Stefan Semukhin, Pavel Widdershoven, Cas model checking Markov chains branching processes automata computational complexity (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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stefan Kiefer and Pavel Semukhin and Cas Widdershoven 2021 Is Part Of LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2021.6 urn:nbn:de:0030-drops-143834 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.6 eng https://creativecommons.org/licenses/by/4.0/legalcode