Petri Nets and Higher-Dimensional Automata

TL;DR

This paper revisits Petri nets by translating them into higher-dimensional automata to better capture true concurrency, extending the approach to include inhibitor arcs and self-modifying nets, and providing a supporting tool.

Contribution

It extends the translation of Petri nets into HDAs to cover inhibitor arcs and self-modifying features, enhancing the modeling of concurrency.

Findings

Successful translation of Petri nets with inhibitor arcs into HDAs

Extended semantics to include self-modifying nets

Implementation of a tool for these translations

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.