Persistent Permutability Implies Persistence for Pure Dissymmetric Choice Petri Nets
摘要
Persistence is a strong, global, behavioural property of a Petri net, meaning that no activity (represented by a transition of the net) can disable a different transition. Persistent permutability is a comparatively local, weaker, property pertaining only to the individual interleavings of a Petri net. We prove that in pure, dissymmetric choice, Petri nets, persistent permutability already suffices to imply persistence. Dissymmetric choice Petri nets generalise free-choice Petri nets and are related to Petri’s notion of “asymmetric confusion”.