Compiling Petri Net Mutual Reachability in Presburger

TL;DR

This paper presents a method to compile the mutual reachability relation of Petri nets into a quantifier-free Presburger formula, improving understanding of their computational complexity and applications.

Contribution

It introduces a novel compilation technique translating Petri net mutual reachability into a doubly exponential disjunction of linear constraints in Presburger arithmetic.

Findings

Compiled mutual reachability into quantifier-free Presburger formulas.

Provided bounds on the size and complexity of the formulas.

Initial results on encoding bottom configurations in Presburger.

Abstract

Petri nets are a classical model of concurrency widely used and studied in formal verification with many applications in modeling and analyzing hardware and software, data bases, and reactive systems. The reachability problem is central since many other problems reduce to reachability questions. The reachability problem is known to be decidable but its complexity is extremely high (non primitive recursive). In 2011, a variant of the reachability problem, called the mutual reachability problem, that consists in deciding if two configurations are mutually reachable was proved to be exponential-space complete. Recently, this problem found several unexpected applications in particular in the theory of population protocols. While the mutual reachability problem is known to be definable in the Preburger arithmetic, the best known upper bound of such a formula was recently proved to be non-elementary (tower). In this paper we provide a way to compile the mutual reachability relation of a Petri net with $d$ counters into a quantifier-free Presburger formula given as a doubly exponential disjunction of $O(d)$ linear constraints of exponential size. We also provide some first results about Presburger formulas encoding bottom configurations.