An axiomatization of the Token Game based on Petri Algebras

International audienceThe firing rule of Petri nets relies on a residuation operation for the commutative monoidof natural numbers. We identify a class of residuated commutative monoids, called Petri algebras,for which one can mimic the token game of Petri nets to define the behaviour of generalized Petrinets whose flow relations and place contents are valued in such algebraic structures. The sum and itsassociated residuation capture respectively how resources within places are produced and consumedthrough the firing of a transition. We show that Petri algebras coincide with the positive cones oflattice-ordered commutative groups and constitute the subvariety of the (duals of) residuated latticesgenerated by the commutative monoid of natural numbers. We however exhibit a Petri algebrawhose corresponding class of nets is strictly more expressive than the class of Petri nets. Moreprecisely, we introduce a class of nets, termed lexicographic Petri nets, that are associated with thepositive cones of the lexicographic powers of the additive group of real numbers. This class ofnets is universal in the sense that any net associated with some Petri algebra can be simulated bya lexicographic Petri net. All the classical decidable properties of Petri nets however (termination,covering, boundedness, structural boundedness, accessibility, deadlock, liveness ...) are undecidableon the class of lexicographic Petri nets. Finally we turn our attention to bounded nets associatedwith Petri algebras and show that their dynamic can be reformulated in term of MV-algebra