Polynomial order algorithms for structural and behavioral analysis of state machine allocatable nets

State machine decomposable nets (SMD nets) are a class of Petri nets which can be decomposed by a set of strongly connected state machines. State machine allocatable nets (SMA nets) are a class of SMD nets, for which well-behavedness such as liveness and safeness of state machine components is preserved in the composed net. The authors propose an efficient polynomial order algorithm to decide whether a given net is a live and safe SMA net or net. The problem can be divided into three sub-problems: (1) to decide if a given net is an SMA net or not, (2) to decide if a given SMA net is live or not, and (3) to decide if a given live SMA net is safe or not. A polynomial order algorithm for the first problem is described. Efficient algorithms for problems (2) and (3) are presented. The algorithms proposed here are based on net decomposition techniques