This paper presents an automated protocol synthesizer which generates the peer entity from a single given local entity. The particular protocol synthesis problem solved is one that will generate the peer entity model such that their interactions are complete, bounded, live, deadlock free, and properly terminated when given a single local entity model.

The procedure discussed consists of five steps: (1) design a local entity model using Petri nets, (2) translate the local entity model into its state transition graph, (3) ensure that the local entity model is well behaved, (4) construct the peer state transition graph, and (5) construct the peer entity model in Petri nets. The input to the program is the Petri net of the given entity and the output will be the Petri net specification of its peer entity.

Several examples that illustrate the Synthesis program are presented. The first one is a packet radio network protocol; the other is a modified X.21 protocol.

The automated synthesis procedure can also be extended to unreliable communication links and N-party communication protocols. These extensions are briefly discussed.

This synthesis procedure is guaranteed to produce protocols which are logically correct if the given local entity model possesses certain local properties. Existing approaches, such as those proposed by Sidhu [1] and Zafiropulo [2] may not guarantee logical correctness of the designed protocol, according to the authors.