Long-Run Average Behaviour of Probabilistic Vector Addition Systems

TL;DR

This paper investigates the long-term pattern frequencies in probabilistic vector addition systems, showing finiteness and computability results for one- and two-counter cases, and challenging some classical assumptions in stochastic Petri nets.

Contribution

It establishes that pattern frequency vectors are well-defined and finitely many for certain probabilistic systems, with polynomial-time approximation for one-counter systems, and provides counterexamples to classical Petri net results.

Findings

Pattern frequency vectors are finite for almost all runs in one-counter pVASS.

These vectors can be approximated in polynomial time for one-counter pVASS.

Counterexamples challenge classical results in stochastic Petri nets.

Abstract

We study the pattern frequency vector for runs in probabilistic Vector Addition Systems with States (pVASS). Intuitively, each configuration of a given pVASS is assigned one of finitely many patterns, and every run can thus be seen as an infinite sequence of these patterns. The pattern frequency vector assigns to each run the limit of pattern frequencies computed for longer and longer prefixes of the run. If the limit does not exist, then the vector is undefined. We show that for one-counter pVASS, the pattern frequency vector is defined and takes only finitely many values for almost all runs. Further, these values and their associated probabilities can be approximated up to an arbitrarily small relative error in polynomial time. For stable two-counter pVASS, we show the same result, but we do not provide any upper complexity bound. As a byproduct of our study, we discover counterexamples falsifying some classical results about stochastic Petri nets published in the~80s.