Issue No. 11 - November (1990 vol. 16)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.60315
<p>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.</p>
formal analysis; formal verification; alternating bit protocol; temporal Petri nets; firings; transitions; formulas; temporal operators; formal specification; omega -regular expressions; Buchi-automata; automata theory; formal specification; Petri nets; program verification; programming theory
I. Suzuki, "Formal Analysis of the Alternating Bit Protocol by Temporal Petri Nets," in IEEE Transactions on Software Engineering, vol. 16, no. , pp. 1273-1281, 1990.