This is the final 'author version', nearly identical to the version published in JACM. 58 pages. This paper previously had the title 'Elements of Petri nets and processes'
We present a formalism for Petri nets based on polynomial-style finite-set configurations and etale maps. The formalism supports both a geometric semantics in the style of Goltz and Reisig (processes are etale maps from graphs) and an algebraic semantics in the style of Meseguer and Montanari, in terms of free coloured props, and allows the following unification: for P a Petri net, the Segal space of P-processes is shown to be the free coloured prop-in-groupoids on P. There is also an unfolding semantics à la Winskel, which bypasses the classical symmetry problems: with the new formalism, every Petri net admits a universal unfolding, which in turn has associated an event structure and a Scott domain. Since everything is encoded with explicit sets, Petri nets and their processes have elements. In particular, individual-token semantics is native. (Collective-token semantics emerges from rather drastic quotient constructions à la Best-Devillers, involving taking π_0 of the groupoids of states.)
The reachability semantics for Petri nets can be studied using open Petri nets. For us an "open" Petri net is one with certain places designated as inputs and outputs via a cospan of sets. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Open Petri nets can be treated as morphisms of a category $\mathsf{Open}(\mathsf{Petri})$, which becomes symmetric monoidal under disjoint union. However, since the composite of open Petri nets is defined only up to isomorphism, it is better to treat them as morphisms of a symmetric monoidal double category $\mathbb{O}\math…
In a previous paper we introduced immediate observation Petri nets, a subclass of Petri nets with application domains in distributed protocols (population protocols) and theoretical chemistry (chemical reaction networks). IO nets enjoy many useful properties, but like the general case of conservative Petri nets they have a PSPACE-complete reachability problem. In this paper we explore two restrictions of the reachability problem for IO nets which lower the complexity of the problem drastically. The complexity is NP-complete for the first restriction with applications in distributed protocols, …
Developing algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms. Petri nets with transits allow us to follow the data flow between components in a distributed system. They can be model checked against specifications in LTL on both the local data flow and the global behavior. Petri games allow the synthesis of local controllers for distributed systems from safety specifications. Modeling problems in these formalisms requires defining extended Petri nets which can be cumbersome wh…
We provide an Ackermannian complexity lower bound for the reachability problem for checking programs, a model equivalent to Petri nets. Moreover in fixed dimension $2d+4$, we show that the problem is $\mathbb{F}_d$-hard. As a direct corollary, the reachability problem in dimension 10 is not elementary.
We introduce stochastic decision Petri nets (SDPNs), which are a form of stochastic Petri nets equipped with rewards and a control mechanism via the deactivation of controllable transitions. Such nets can be translated into Markov decision processes (MDPs), potentially leading to a combinatorial explosion in the number of states due to concurrency. Hence we restrict ourselves to instances where nets are either safe, free-choice and acyclic nets (SAFC nets) or even occurrence nets and policies are defined by a constant deactivation pattern. We obtain complexity-theoretic results for such cases …
Solutions proposed for the longstanding problem of automatic decomposition of Petri nets into concurrent processes, as well as methods developed in Grenoble for the automatic conversion of safe Petri nets to NUPNs (Nested-Unit Petri Nets), require certain properties to be computed on Petri nets. We notice that, although these properties are theoretically interesting and practically useful, they are not currently implemented in mainstream Petri net tools. Taking into account such properties would open fruitful research directions for tool developers, and new perspectives for the Model Checking …
In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no…
To model check concurrent systems, it is convenient to distinguish between the data flow and the control. Correctness is specified on the level of data flow whereas the system is configured on the level of control. Petri nets with transits and Flow-LTL are a corresponding formalism. In Flow-LTL, both the correctness of the data flow and assumptions on fairness and maximality for the control are expressed in linear time. So far, branching behavior cannot be specified for Petri nets with transits. In this paper, we introduce Flow-CTL* to express the intended branching behavior of the data flow w…
SMPT (for Satisfiability Modulo Petri Net) is a model checker for reachability problems in Petri nets. It started as a portfolio of methods to experiment with symbolic model checking, and was designed to be easily extended. Some distinctive features are its ability to benefit from structural reductions and to generate verdict certificates. Our tool is quite mature and performed well compared to other state-of-the-art tools in the Model Checking Contest.
Petri nets are a mathematical language for modeling and reasoning about distributed systems. In this paper we propose an approach to Petri nets for embedding reversibility, i.e., the ability of reversing an executed sequence of operations at any point during operation. Specifically, we introduce machinery and associated semantics to support the three main forms of reversibility namely, backtracking, causal reversing, and out-of-causal-order reversing in a variation of cyclic Petri nets where tokens are persistent and are distinguished from each other by an identity. Our formalism is influenced…
State Space Computation and Analysis of Time Petri Nets
Petri网理论提供了一个通用的框架来描述实时反应式系统的行为，时间Petri网的引入也考虑了时间规范。本文提出了一种基于前向区域的算法来计算有界时间Petri网的状态空间：该方法与经典的状态类图不同，并且更有效。我们证明该算法是精确的可达性问题。此外，我们提出了一个翻译的计算状态空间到一个时间自动机，证明了原来的时间Petri网的时间双相似。当该方法产生单个时间自动机时，可以应用语法时钟减少方法（例如Daws和Yovine）来产生具有更少时钟的自动机。然后，我们的方法允许通过使用高效的时间自动机工具进行模型检查TTPN。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
We provide a categorical semantics for bounded Petri nets, both in the collective- and individual-token philosophy. In both cases, we describe the process of bounding a net internally, by just constructing new categories of executions of a net using comonads, and externally, using lax-monoidal-lax functors. Our external semantics is non-local, meaning that tokens are endowed with properties that say something about the global state of the net. We then prove, in both cases, that the internal and external constructions are equivalent, by using machinery built on top of the Grothendieck construct…
On detectability of labeled Petri nets and finite automata
我们研究了标记Petri网和有限自动机的可检测性。我们首先研究弱近似可检测性（WAD），这意味着存在一个无限的观察系统的输出序列，使每个前缀的输出序列的长度大于一个给定的值允许观察者确定当前状态属于一个给定的集合。我们还考虑了两个新的概念，称为即时强探测能力（ISD）和最终强探测能力（ESD）。前一个属性意味着对于每个可能的无限观测输出序列，输出序列的每个前缀允许重构当前状态。后者意味着对于每个可能的无限观测输出序列，存在一个值，使得长度大于该值的输出序列的每个前缀允许重构当前状态。结果如下：WAD：不可判定的标记Petri网，PSPACE-完全的有限自动机ISD：decidable and EXPSPACE-hard for labeled Petri nets，属于P有限自动机ESD：decidable under proximity assumption and EXPSPACE-hard for labeled Petri nets，属于P有限自动机SD：属于有限自动机的P，基于无死锁和无约束两个假设，加强了Shu和Lin在2011年的结果，ISD<SD<ESD<WD<WAD，用于标记Petri网和有限自动机
