Model checking stochastic branching processes.

*(English)*Zbl 1365.68320
Rovan, Branislav (ed.) et al., Mathematical foundations of computer science 2012. 37th international symposium, MFCS 2012, Bratislava, Slovakia, August 27–31, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32588-5/pbk). Lecture Notes in Computer Science 7464, 271-282 (2012).

Summary: Stochastic branching processes are a classical model for describing random trees, which have applications in numerous fields including biology, physics, and natural language processing. In particular, they have recently been proposed to describe parallel programs with stochastic process creation. In this paper, we consider the problem of model checking stochastic branching process. Given a branching process and a deterministic parity tree automaton, we are interested in computing the probability that the generated random tree is accepted by the automaton. We show that this probability can be compared with any rational number in PSPACE, and with 0 and 1 in polynomial time. In a second part, we suggest a tree extension of the logic PCTL, and develop a PSPACE algorithm for model checking a branching process against a formula of this logic. We also show that the qualitative fragment of this logic can be model checked in polynomial time.

For the entire collection see [Zbl 1246.68054].

For the entire collection see [Zbl 1246.68054].