A Petri Net Model of Handshake Protocols

We propose a Petri net model of handshake protocols. These are asynchronous communication protocols which enforce several properties such as absence of transmission interference and insensitivity from delays of propagation on wires. We introduce the notion of handshake Petri net, a Petri net with a specific external interface. We show that the set of observable quiescent traces generated by such a net captures the properties defining a handshake protocol. Conversely we show that for any handshake protocol we can construct a corresponding net. We also study different subclasses of the model. Many examples are provided.