Petri Nets and Higher-Dimensional Automata

TL;DR

Petri nets are a canonical model of concurrency but are often treated with interleaving semantics, which obscure true concurrency. The paper presents a translation from Petri nets to higher-dimensional automata (HDAs) in an event-based setting, extending it to Petri nets with inhibitor arcs (PNIs) under both a-posteriori and a-priori semantics, and to generalized self-modifying nets (G-nets) via ST-graphs and ST-automata. It demonstrates correspondences between Petri-net semantics and HDAs, enabling precise reasoning about concurrency through concepts like truncation and flattening, and provides a prototype tool (pn2HDA) that implements these translations for standard, weighted, and inhibitor-arc nets, as well as PNIs to partial HDAs and G-nets to ST-graphs. The work establishes a unifying framework for concurrent semantics across Petri nets variants and lays groundwork for extensions to time and real-time con gurations, supported by a working toolchain and examples.

Abstract

Petri nets and their variants are often considered through their interleaved semantics, i.e. considering executions where, at each step, a single transition fires. This is clearly a miss, as Petri nets are a true concurrency model. This paper revisits the semantics of Petri nets as higher-dimensional automata (HDAs) as introduced by van Glabbeek, which methodically take concurrency into account. We extend the translation to include some common features. We consider nets with inhibitor arcs, under both concurrent semantics used in the literature, and generalized self-modifying nets. Finally, we present a tool that implements our translations.

Figures (2)

• Figure 1: Petri nets and HDAs for interleaving (left) and true concurrency (right).
• Figure 2: A two-dimensional HDA $X$ on $\Sigma=\{a, c, d\}$, see Ex. \ref{['ex:hda']}.

Theorems & Definitions (1)

• remark thmcounterremark