Synthesis approach for designing concurrent systems

Summary form only given, as follows. The complexity of verifying a concurrent system grows exponentially as the number of functions and states in the system increases. To avoid this state explosion problem the authors propose a synthesis approach, thus eliminating the need for design verification. This approach uses a Petri net modeling the concurrent system to be designed. At each synthesis step, the Petri net is expanded by adding places and transitions to the net according to some rules. These rules are devised so that after each synthesis step, the resulting net is logically correct. The authors illustrate the method by using a two-party protocol design as an example. Finally, they show that this rule-based approach allows the possibility of automation with a resulting close control of concurrency in the system.