Zero-Safe Nets: Composing Nets via Transition Synchronization

Zero-safe nets have been introduced to extend classical Petri nets with a primitive notion of transition synchronization. To this aim, besides ordinary places, called stable, zero-safe nets are equipped with zero places, which cannot contain any token in a stable marking. An evolution between two stable markings is called transaction and can be a complex computation that involves zero places, with the restriction that no stable token generated in a transaction can be reused in the same transaction. The abstract counterpart of a generic zero-safe net B consists of an ordinary PT net whose places are the stable places of B, and whose transitions are the transactions of B. The two nets offer the refined and the abstract model of the same system, where the former can be much smaller than the latter, because of the transition synchronization mechanism. Depending on the chosen approach -- collective vs individual token philosophy -- two notions of transaction may be defined, each leading to different operational and abstract models. We survey the two approaches, discussing their main properties and showing several applications.