Invariant-preserving transformations for the verification of place/transition systems (with application to the verification of protocols).

Abstract

Transformations preserving specific properties are often used for the verification of place/transition systems. They simplify a system so that some designated properties can be detected more easily from the simplified system but are still valid for the original one. This thesis presents five general classes of transformations on place/transition systems (PTSs), namely, insertion, elimination, replacement, composition and decomposition, and the conditions for them to preserve place-invariants and transition-invariants of the PTSs. Also proposed is a special transformation for eliminating isolatable places. It leads to the proposal of a constructive algorithm for finding place invariants. The algorithm simplifies a PTS iteratively in such a way that its place-invariants can be derived from those of the simplified ones. Lastly, some of these transformations and the algorithm are applied to find place-invariants for two classes of the Transport Protocol.