Event Structures for Petri nets with Persistence

TL;DR

This paper extends the connection between Petri nets and event structures to include disjunctive causes by introducing Petri nets with persistence, linking them to locally connected event structures through an unfolding construction.

Contribution

It introduces Petri nets with persistence to model disjunctive causes and establishes their correspondence with locally connected event structures.

Findings

Disjunctive causes are modeled by persistent places in Petri nets.

Petri nets with persistence relate to locally connected event structures.

A chain of coreflections formalizes the connection between nets and event structures.

Abstract

Event structures are a well-accepted model of concurrency. In a seminal paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge between the theory of domains and the approach to concurrency proposed by Petri. A basic role is played by an unfolding construction that maps (safe) Petri nets into a subclass of event structures, called prime event structures, where each event has a uniquely determined set of causes. Prime event structures, in turn, can be identified with their domain of configurations. At a categorical level, this is nicely formalised by Winskel as a chain of coreflections. Contrary to prime event structures, general event structures allow for the presence of disjunctive causes, i.e., events can be enabled by distinct minimal sets of events. In this paper, we extend the connection between Petri nets and event structures in order to include disjunctive causes. In particular, we show that, at the level of nets, disjunctive causes are well accounted for by persistent places. These are places where tokens, once generated, can be used several times without being consumed and where multiple tokens are interpreted collectively, i.e., their histories are inessential. Generalising the work on ordinary nets, Petri nets with persistence are related to a new subclass of general event structures, called locally connected, by means of a chain of coreflections relying on an unfolding construction.