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.

翻译：Petrinet是典型的货币模型,在正式核查中广泛使用和研究,许多应用在硬件和软件、数据库和反应系统模型和分析中广泛使用和研究。可达性问题是核心问题,因为许多其他问题都减少了可达性问题。已知可达性问题是可以分解的,但其复杂性极高(非原始再现性),2011年,可达性问题的一个变体,称为相互可达性问题,即决定两个配置是否可相互可达性被证明是指数-空间完成的。最近,这个问题发现若干出乎意料的应用,特别是在人口协议理论中。虽然在预堡计算中可以确定相互可达性问题,但已知的这种公式的最佳上限最近证明是非基本性(tower) 。在本文中,我们提供了一种方法,将Petrii net与$d$对等的可互达性连接关系编成一个量化的无孔径方方公式,作为指数大小的美元(d)线性限制的指数分解。我们还提供了一些关于Presburgergins 公式底质配置的初步结果。