Invariant-preserving transformations for the verification of place/transition systems

Transformations preserving (i.e., neither losing nor creating) specific properties are often used to simplify a system so that certain specified properties can be detected more easily from the transformed system. For five classes of transformations on place/transition systems (PTSs), namely, insertion, elimination, replacement, composition and decomposition, this paper provides the conditions which can be used for determining whether or not they preserve the place-invariants and transition-invariants of the PTS. A place-invariant is a subset of places whose total number of tokens remains unchanged under any execution of the system. A transition-invariant is a multiset of transitions whose execution in a certain order will leave the distribution of tokens unchanged. Unlike the basic approach of detecting place-invariants, which requires lengthy computation on the entire system of row matrix equations, the proposed conditions are for very general transformations and involve computation of only the new, eliminated and affected places and transitions