Ugo Montanari (Università di Pisa):
Zero-Safe Nets: Composing Nets via Transition Synchronization
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.
Colloquium home page
