Detection of livelocks in communication protocols by means of a polygon time structure

As has been shown, the polygon time structure overcomes the main limitations of the interval time structure, and allows one to verify communication protocols, in which the explicit concurrency of both competing and supporting events is considered. The authors apply the polygon time structure to the verification of dynamic properties (like livelocks) of a simple protocol. As a result, they show that an application of the previously used interval time structure may lead to the evaluation of a protocol as incorrect, while it is livelock free.