Linear-Time Model Checking Branching Processes

TL;DR

This paper investigates the complexity of verifying whether infinite trees generated by multi-type branching processes satisfy linear-time omega-regular specifications, establishing a PSPACE complexity result for LTL properties.

Contribution

It introduces a PSPACE complexity classification for model checking branching processes against LTL specifications, extending classical results from transition systems and Markov chains.

Findings

Model checking is in PSPACE for LTL specifications.

Automata-theoretic approach using unambiguous Büchi automata.

Generalizes classical results to branching processes.

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\"uchi automata.