M.: On the Importance of the Deadlock Trap Property for Monotonic Liveness

Abstract. In Petri net systems, liveness is an important property cap-turing the idea of no transition (action) becoming non-fireable (unattain-able). Additionally, in some situations it is particularly interesting to check if the net system is (marking) monotonically live, i.e., it remains live for any marking greater than the initial one. In this paper, we dis-cuss structural conditions preserving liveness under arbitrary marking increase. It is proved that the deadlock trap property (DTP) is a neces-sary condition for liveness monotonicity of ordinary nets, and necessary and sufficient for some subclasses. We illustrate also how the result can be used to study liveness monotonicity for non-ordinary nets using a sim-ulation preserving the firing language. Finally, we apply these conditions to several case studies of biomolecular networks.