Introducing Divergence for Infinite Probabilistic Models
Alain Finkel, Serge Haddad, Lina Ye
TL;DR
The paper introduces the divergence property for infinite-state Markov chains to enable computing reachability probabilities ${\bf Pr}_{\mathcal{M},s_0}({\bf F}A)$ up to arbitrary precision without requiring decidability, and presents two generic CRP algorithms that work with or without decidability assumptions. It establishes decidability and undecidability boundaries for divergence in models such as random walks and probabilistic Petri nets, and provides concrete divergent-by-construction model classes, notably probabilistic open channel systems and increasing probabilistic pushdown automata. It also develops sufficient conditions via martingale-inspired techniques to certify divergence and demonstrates how these ideas can be leveraged in open-queueing networks and other dynamic systems. The work aims to enable practical quantitative analysis of congested and open distributed systems by offering generic, model-agnostic procedures for CRP and by identifying tractable divergent subclasses for realistic modeling scenarios.
Abstract
Computing the reachability probability in infinite state probabilistic models has been the topic of numerous works. Here we introduce a new property called divergence that when satisfied allows to compute reachability probabilities up to an arbitrary precision. One of the main interest of divergence is that this computation does not require the reachability problem 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. where probabilities related to service requirements are needed.
