Reachability analysis of branching probabilistic processes
Martinov, Emanuel Ognyanov
We study a fundamental class of infinite-state stochastic processes and stochastic games, namely Branching Processes, under the properties of (single-target) reachability and multi-objective reachability. In particular, we study Branching Concurrent Stochastic Games (BCSGs), which are an imperfect-information game extension to the classical Branching Processes, and show that these games are determined, i.e., have a value, under the fundamental objective of reachability, building on and generalizing prior work on Branching Simple Stochastic Games and finite-state Concurrent Stochastic Games. We show that, unlike in the turn-based branching games, in the concurrent setting the almost-sure and limitsure reachability problems do not coincide and we give polynomial time algorithms for deciding both almost-sure and limit-sure reachability. We also provide a discussion on the complexity of quantitative reachability questions for BCSGs. Furthermore, we introduce a new model, namely Ordered Branching Processes (OBPs), which is a hybrid model between classical Branching Processes and Stochastic Context-Free Grammars. Under the reachability objective, this model is equivalent to the classical Branching Processes. We study qualitative multi-objective reachability questions for Ordered Branching Markov Decision Processes (OBMDPs), or equivalently context-free MDPs with simultaneous derivation. We provide algorithmic results for efficiently checking certain Boolean combinations of qualitative reachability and non-reachability queries with respect to different given target non-terminals. Among the more interesting multi-objective reachability results, we provide two separate algorithms for almost-sure and limit-sure multi-target reachability for OBMDPs. Specifically, given an OBMDP, given a starting non-terminal, and given a set of target non-terminals, our first algorithm decides whether the supremum probability, of generating a tree that contains every target non-terminal in the set, is 1. Our second algorithm decides whether there is a strategy for the player to almost-surely (with probability 1) generate a tree that contains every target non-terminal in the set. The two separate algorithms are needed: we show that indeed, in this context, almost-sure and limit-sure multi-target reachability do not coincide. Both algorithms run in time polynomial in the size of the OBMDP and exponential in the number of targets. Hence, they run in polynomial time when the number of targets is fixed. The algorithms are fixed-parameter tractable with respect to this number. Moreover, we show that the qualitative almost-sure (and limit-sure) multi-target reachability decision problem is in general NP-hard, when the size of the set of target non-terminals is not fixed.