Zero-safe nets: The individual token approach

In this paper we provide both an operational and an abstract concurrent semantics for zero-safe nets under the individual token philosophy. The main feature of zero-safe nets is a primitive notion of transition synchronization. Besides ordinary places, called stable places, zero-saf nets come equipped with zero places, which are empty in any stable marking. Connected transactions represent basic atomic computations of the system between stable markings. They must satisfy two main requirements: 1) to model interacting activities which cannot be decomposed into disjoint sub-activities, and 2) not to consume stable tokens which were generated in the same transaction. Zero tokens acts as triggers for the firings of the transitions which compose the transaction. The abstract counterpart of a zero-safe net consists of a P/T net where each transition locates a distinguished transaction. In the second part of the paper, following the Petri nets are monoids approach, we make use of category theory to analyze and motivate our framework. More precisely, the operational semantics of zero-safe nets is characterized as an adjunction, and the derivation of abstract P/T nets as a coreflection.