A necessary and sufficient condition for SMA nets
D.-I. Lee, Satoshi Kumagai, Shinzo Kodama · 1991
The aim is to clarify the restrictions on strongly connected state machine (SCSM) composition for state machine allocatable nets (SMA nets). The problem can be viewed as finding the structure of the synchronization between SCSMs to yield relevant properties such as SMA nets. The importance of investigating the structural properties of the SMA net can be understood by the fact that a free choice net is live and safe iff the net is an SMA net. Moreover, to synthesize a live and safe free choice net is often the goal of correct concurrent system design. A necessary and sufficient condition for a net composition to guarantee that the net falls into an important subclass of Petri nets is presented.>