Formal analysis of the alternating bit protocol by temporal Petri nets

摘要

Temporal Petri nets are Petri nets in which certain restrictions on the firings of transitions are represented by formulas containing temporal operators. The use of temporal Petri nets for formal specification and verification of the alternating bit protocol is discussed. The temporal Petri net which models the protocol is analyzed formally using the existing theory of omega -regular expressions and Buchi-automata.