The knitting technique and its application to communication protocol synthesis

The Petri net (PN) can be incrementally expanded by adding paths of nodes according to the synthesis rules. These paths of nodes are generated to increase the number of concurrent, conditional, and iterative processes. A set of synthesis rules has been developed to ensure the correct generation of these paths of nodes. The advantages of these rules include the possibility of implementation as a CAD tool, the guarantee of liveness, boundedness, and reversibility (well-behaved properties), and the close control of concurrency and nondeterminism. These rules serve two functions for interactive design: prevention of potential problems and guidance of correct new path generations. Examples of synthesis and a procedure of finding invariants are presented to show that one can synthesize PNs beyond asymmetric-choice nets. The technique is applied to the synthesis of communication protocols and extended to synthesize local entities