In: Automatic Control and Computer Sciences, Vol. 22, No. 5, pages 17-21. 1988.
Abstract: The authors identify a subset of static correctness properties of protocols. A class of predicate-time Petri nets is introduced to analyze these properties. A modified Farkas algorithm is proposed for matrix calculation of the systems of invariants of the model. Logical assertions are formulated that are required for analyzing correctness properties.