Facial reconstruction

Search LJMU Research Online

Browse Repository | Browse E-Theses

Linear-Time Model Checking Branching Processes

Semukhin, P, Kiefer, S and Widdershoven, C (2021) Linear-Time Model Checking Branching Processes. In: LIPIcs : Leibniz International Proceedings in Informatics , 203 (6). 6:1-6:16. (32nd International Conference on Concurrency Theory (CONCUR 2021), 24 August 2021 - 27 August 2021, Virtual Event).

Linear-Time Model Checking Branching Processes.pdf - Published Version
Available under License Creative Commons Attribution.

Download (676kB) | Preview


(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.

Item Type: Conference or Workshop Item (Paper)
Uncontrolled Keywords: model checking; Markov chains; branching processes; automata; computational complexity
Subjects: Q Science > QA Mathematics > QA75 Electronic computers. Computer science
Divisions: Computer Science & Mathematics
Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Date Deposited: 25 Feb 2022 11:14
Last Modified: 13 Apr 2022 15:18
URI: https://researchonline.ljmu.ac.uk/id/eprint/16415
View Item View Item