Model Checking Stochastic Branching Processes

DOI10.1007/978-3-642-32589-2_26MaRDI QIDQ2912726zbMATH OpenOpenAlexFDO

Authors Taolue Chen, Klaus Dräger, Stefan Kiefer

Publication date 25 September 2012

Published in Mathematical Foundations of Computer Science 2012 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1206.1317

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Stochastic model checking
• Linear-Time Model Checking Branching Processes
• Model checking stochastic automata
• scientific article; zbMATH DE number 2079828
• Model-checking continuous-time Markov chains
• Branching-time model-checking of probabilistic pushdown automata
• Branching-time model-checking of probabilistic pushdown automata
• Computer Aided Verification
• Symbolic model checking for probabilistic processes
• Model checking probabilistic systems

Cited in

(9)

• Model checking stochastic automata
• Model-free reinforcement learning for branching Markov decision processes
• scientific article; zbMATH DE number 7561608 (Why is no real title available?)
• The uniform measure of simple regular sets of infinite trees
• Separable GPL: decidable model checking with more non-determinism
• Computing measures of weak-mso definable sets of trees
• scientific article; zbMATH DE number 7447744 (Why is no real title available?)
• Stochastic Process Creation
• scientific article; zbMATH DE number 2079828 (Why is no real title available?)

This page was built for publication: Model Checking Stochastic Branching Processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2912726)