Zero-Safe Nets, or Transition Synchronization Made Simple

In addition to ordinary places, called stable, zero-safe nets are equipped with zero places, which in a stable marking cannot contain any token. An evolution between two stable markings, instead, can be a complex computation called stable transaction, which may use zero places, but which is atomic when seen from stable places: no stable token generated in a transaction can be reused in the same transaction. Every zero-safe net has an ordinary Place-Transition net as its abstract counterpart, where only stable places are maintained, and where every transaction becomes a transition. The two nets allow us to look at the same system from both an abstract and a refined viewpoint. To achieve this result no new interaction mechanism is used, besides the ordinary token-pushing rules of nets. The refined zero-safe nets can be much smaller than their corresponding abstract P/T nets, since they take advantage of a transition synchronization mechanism. For instance, when transactions of unlimited length are possible in a zero safe net, the abstract net becomes infinite, even if the refined net is finite. In the second part of the paper two universal constructions - both following the Petri nets are monoids approach and the collective token philosophy - are used to give evidence of the naturality of our definitions. 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.