Introducing Divergence for Infinite Probabilistic Models

Abstract

Computing the reachability probability in infinite state probabilistic models has been the topic of numerous works. Here we introduce a new property called \emph{divergence} that when satisfied allows to compute reachability probabilities up to an arbitrary precision. One of the main interests of divergence is that this computation does not require the reachability problem, i.e., the possibility to reach target states from an initial state in a given model, to be decidable. Then we study the decidability of divergence for random walks and the probabilistic versions of Petri nets where the weights associated with transitions may also depend on the current state. This should be contrasted with most of the existing works that assume weights independent of the state. Such an extended framework is motivated by the modeling of real case studies. Moreover, we exhibit some subclasses of channel systems and pushdown automata that are divergent by construction, particularly suited for specifying open distributed systems and networks prone to performance collapsing where probabilities related to service requirements are needed.