Analysis of Probabilistic Basic Parallel Processes

TL;DR

This paper investigates the decidability and complexity of key qualitative problems in probabilistic Basic Parallel Processes, a subclass of Petri Nets modeling concurrent systems with probabilistic spawning, covering both Markov chain and MDP models.

Contribution

It provides new results on the decidability and complexity of reachability problems in probabilistic BPPs, addressing both Markov chains and MDPs.

Findings

Decidability results for reachability with probability 1.

Complexity classifications for various classes of target sets.

Analysis of probabilistic BPPs in both Markov chain and MDP frameworks.

Abstract

Basic Parallel Processes (BPPs) are a well-known subclass of Petri Nets. They are the simplest common model of concurrent programs that allows unbounded spawning of processes. In the probabilistic version of BPPs, every process generates other processes according to a probability distribution. We study the decidability and complexity of fundamental qualitative problems over probabilistic BPPs -- in particular reachability with probability 1 of different classes of target sets (e.g. upward-closed sets). Our results concern both the Markov-chain model, where processes are scheduled randomly, and the MDP model, where processes are picked by a scheduler.