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

翻译：分支过程( 多型) 分支过程是一种天然的、 研究周密的生成随机无限树的模型。 分支过程既具有非确定性和概率性的分支, 也具有非确定性和概率性的分支, 包括过渡系统和Markov 链条( 但一般而言不是Markov 决策程序 ) 。 我们根据线性时间的 omega- 常规规格研究模型检查分支过程的复杂性: 分枝过程随机生成的树枝的每个分支都符合 omega- 常规规格, 这几乎可以肯定吗? 主要的结果是对于 LTL 的规格来说, 这个问题在 PSPACE 中, 分别包含过渡系统和Markov 链条的经典结果 。 基本的一般模型检查算法基于自磁理论方法, 使用毫不含糊的 B\\ uchi 自动算法 。