Structural and Behavioral Analysis of State Machine Allocatable Nets Based on Net Decomposition

Dong-Ik LEE  Tadaaki NISHIMURA  Sadatoshi KUMAGAI  

IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E76-A   No.3   pp.399-408
Publication Date: 1993/03/25
Online ISSN: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section on the 5th Karuizawa Workshop on Circuits and Systems)
Petri nets,  SMA nets,  S-decomposition,  S-component,  liveness,  safeness,  algorithm,  

Full Text: PDF(838.8KB)>>
Buy this Article

Free choice nets are a class of Petri nets, which can represent the substantial features of systems by modeling both choice and concurrency. And in the modelling and design of a large number of concurrent systems, live and safe free choice nets (LSFC nets) have been explored their structural characteristics. On the other hand, state machine decomposable nets (SMD nets) are a class of Petri nets which can be decomposed by a set of strongly connected state machines (S-decomposition). State machine allocatable nets (SMA nets) are a well-behaved class of SMD nets. Of particular interest is the relation between free choice nets and SMA nets such that a free choice net has a live and safe marking if and only if the net is an SMA net. That is, the structure of an LSFC net is an SMA net. Recently, the structure of SMA net has been completely characterized by the authors based on an S-decomposition. In other words, a necessary and sufficient condition for a net to be an SMA net is obtained in terms of the net structure where synchronization between strongly connected state machine components (S-components) has been clarified. Unfortunately, it requires tremendous amount of time and spaces to decide a given net to be an SMA net by applying the condition directly. Moreover, there exist no efficient algorithm to decide the liveness and safeness of a given SMA net that lessens the usefulness of decomposition techniques. In this paper, we consider efficient polynomial order algorithms to decide whether a given net is a live and safe SHA net.