INVARIANT-PRESERVING TRANSFORMATIONS FOR THE VERIFICATION OF PLACE TRANSITION SYSTEMS/

Transformations preserving (i.e., neither losing nor creating) specifi c properties are often used to simplify a system so that certain speci fied properties can be detected more easily from the transformed syste m, For five classes of transformations on place/transition systems (PT S's), namely, insertion, elimination, replacement, composition, and de composition, this paper provides the conditions which can be used for determining whether or not they preserve the place-invariants and tran sition-invariants of the PTS, ii 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 un changed. Unlike the basic approach of detecting place-invariants, whic h requires lengthy computation on the entire system of dow matrix equa tions, the proposed conditions are for very general transformations an d involve computation of only the new, eliminated, and affected places and transitions.