In: Proc. 19th Symp. on Reliable Distributed Systems, 16-18 October 2000, Nürnberg, Germany, pages 84-93. 2000.
Abstract: As has been shown, the polygon time structure overcomes the main limitations of the interval time structure, and allows to verify communication protocols, in which the explicit concurrency of both competing and supporting events is considered. Protocols are considered as timed concurrent systems, represented by timed Petri nets. This paper applies the polygon time structure to the verification of dynamic properties (like livelock) of a simple protocol. As a result, an application of the previously used interval time structure may lead to the evaluation of a protocol as incorrect, while it is livelock free.
Keywords: communication protocols, interval time structure, livelock detection, polygon time structure, protocol verification, timed Petri nets.
Back to the Petri Nets Bibliography