Reference:

Taolue Chen, Klaus Dräger, and Stefan Kiefer. Model checking stochastic branching processes. In Vladimiro Sassone and Peter Widmayer, editors, Proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 7464 of LNCS, pages 271–282, Bratislava, Slovakia, 2012. Springer.

Abstract:

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.

Suggested BibTeX entry:

@inproceedings{12CDK:MFCS,
    address = {Bratislava, Slovakia},
    author = {Taolue Chen and Klaus Dr\"ager and Stefan Kiefer},
    booktitle = {Proceedings of the 37th International Symposium on Mathematical Foundations of Computer Science (MFCS)},
    editor = {Vladimiro Sassone and Peter Widmayer},
    pages = {271--282},
    publisher = {Springer},
    series = {LNCS},
    title = {Model Checking Stochastic Branching Processes},
    volume = {7464},
    year = {2012}
}