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.
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copy
Dong-Ik LEE, Tadaaki NISHIMURA, Sadatoshi KUMAGAI, "Structural and Behavioral Analysis of State Machine Allocatable Nets Based on Net Decomposition" in IEICE TRANSACTIONS on Fundamentals,
vol. E76-A, no. 3, pp. 399-408, March 1993, doi: .
Abstract: 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.
URL: https://globals.ieice.org/en_transactions/fundamentals/10.1587/e76-a_3_399/_p
Copy
@ARTICLE{e76-a_3_399,
author={Dong-Ik LEE, Tadaaki NISHIMURA, Sadatoshi KUMAGAI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Structural and Behavioral Analysis of State Machine Allocatable Nets Based on Net Decomposition},
year={1993},
volume={E76-A},
number={3},
pages={399-408},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={March},}
Copy
TY - JOUR
TI - Structural and Behavioral Analysis of State Machine Allocatable Nets Based on Net Decomposition
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 399
EP - 408
AU - Dong-Ik LEE
AU - Tadaaki NISHIMURA
AU - Sadatoshi KUMAGAI
PY - 1993
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E76-A
IS - 3
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - March 1993
AB - 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.
ER -