Introducing Divergence for Infinite Probabilistic Models

TL;DR

This paper introduces the concept of divergence in infinite probabilistic models, enabling approximate reachability probability computation without requiring decidability of reachability, and explores its decidability and applications in various models.

Contribution

It proposes divergence as a new property for probabilistic models, allowing probability computation without reachability decidability, and analyzes its decidability in different models including Petri nets and automata.

Findings

Divergence allows approximate reachability probability computation.

Decidability of divergence varies across models like random walks and Petri nets.

Certain subclasses of systems are inherently divergent, useful for modeling distributed systems.

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.