Toward a Uniform Approach to the Unfolding of Nets

TL;DR

This paper introduces spread nets, a generalized class of Petri nets with vector clocks and ticking functions, enabling a uniform approach to representing concurrent executions with loops in time.

Contribution

It proposes spread nets as a unifying framework that generalizes unfoldings, merged processes, and trellis processes for true concurrency semantics.

Findings

Spread nets generalize existing net families.

They allow loops in time, unlike previous models.

Enable uniform representation of concurrent runs.

Abstract

In this paper we introduce the notion of spread net. Spread nets are (safe) Petri nets equipped with vector clocks on places and with ticking functions on transitions, and are such that vector clocks are consistent with the ticking of transitions. Such nets generalize previous families of nets like unfoldings, merged processes and trellis processes, and can thus be used to represent runs of a net in a true concurrency semantics through an operation called the spreading of a net. By contrast with previous constructions, which may identify conflicts, spread nets allow loops in time