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

Description
Title: Invariant-preserving transformations for the verification of place/transition systems (with application to the verification of protocols).
Authors: Zeng, Wei.
Date: 1995
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.
URL: http://hdl.handle.net/10393/9977
http://dx.doi.org/10.20381/ruor-8062
CollectionTh├Ęses, 1910 - 2010 // Theses, 1910 - 2010
Files
MM07813.PDF1.32 MBAdobe PDFOpen