A basic theorem for modular synthesis of state machine allocatable nets

Considers a necessary and sufficient condition for a net composition to guarantee that the composed net falls into an important subclass of Petri nets, called state machine allocatable (SMA) nets. The structural properties of SMA nets based on strongly connected state machine (SCSM)-components have been obtained by the authors. The aim is to strengthen the previous results and to give a necessary and sufficient condition for a net to be an SMA net. It is shown that the conditions are independent of the way of SCSM-decomposition; that is, it suffices to verify the conditions for SCSM-components corresponding to any one of the SCSM-decompositions