Table of Contents
Fetching ...

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.

Introducing Divergence for Infinite Probabilistic Models

TL;DR

The paper introduces the divergence property for infinite-state Markov chains to enable computing reachability probabilities 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.
Paper Structure (13 sections, 17 theorems, 10 equations, 6 figures)

This paper contains 13 sections, 17 theorems, 10 equations, 6 figures.

Key Result

Proposition 2.7

Let $\mathcal{M}$ be a Markov chain, $s_0\in S$, $A\subseteq S$, and a computable function $f$ from $S$ to $\mathbb{R}_{\geq 0}$ such that: Then $\mathcal{M}$ is divergent w.r.t. $s_0$ and $A$.

Figures (6)

  • Figure 1: A random walk $\mathcal{M}_1$
  • Figure 2: An infinite (divergent) Markov chain
  • Figure 3: Illustration of divergence
  • Figure 6: A schematic view of pOCS
  • Figure 7: A simple production system
  • ...and 1 more figures

Theorems & Definitions (34)

  • Definition 2.1: Effective Markov chain
  • Example 2.2
  • Definition 2.3: Irreducibility, recurrence, transience
  • Example 2.4
  • Example 2.5
  • Definition 2.6: divergent Markov chain
  • Proposition 2.7
  • Proposition 2.7
  • Proposition 2.7
  • Theorem 3.0
  • ...and 24 more