A Graph Theoretic Approach to Reachability Problem with Petri Net Unfoldings
Summary :
Petri nets are widely recognized as a powerful model for discrete event systems. Petri nets have both graphical and mathematical features. Graphical feature provides an environment to design and to comprehend discrete event systems. Mathematical feature provides an analysis power for verifying several properties of such systems. Several analysis techniques have been proposed so far, such as a reachability (coverability) graph method, a matrix equation approach, reduction or decomposition techniques, a symbolic model method and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often used in the verification of asynchronous circuits. This paper focuses on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and a upper bound problem. Relations between these problems and an unfolding have been clarified to provide a novel method to resolve these problems.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E79-A No.11 pp.1809-1816
- Publication Date
- 1996/11/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Special Section PAPER (Special Section on Description Models for Concurrent Systems and Their Applications)
- Category
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
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.
Cite this
Copy
Toshiyuki MIYAMOTO, Sadatoshi KUMAGAI, "A Graph Theoretic Approach to Reachability Problem with Petri Net Unfoldings" in IEICE TRANSACTIONS on Fundamentals,
vol. E79-A, no. 11, pp. 1809-1816, November 1996, doi: .
Abstract: Petri nets are widely recognized as a powerful model for discrete event systems. Petri nets have both graphical and mathematical features. Graphical feature provides an environment to design and to comprehend discrete event systems. Mathematical feature provides an analysis power for verifying several properties of such systems. Several analysis techniques have been proposed so far, such as a reachability (coverability) graph method, a matrix equation approach, reduction or decomposition techniques, a symbolic model method and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often used in the verification of asynchronous circuits. This paper focuses on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and a upper bound problem. Relations between these problems and an unfolding have been clarified to provide a novel method to resolve these problems.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e79-a_11_1809/_p
Copy
@ARTICLE{e79-a_11_1809,
author={Toshiyuki MIYAMOTO, Sadatoshi KUMAGAI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={A Graph Theoretic Approach to Reachability Problem with Petri Net Unfoldings},
year={1996},
volume={E79-A},
number={11},
pages={1809-1816},
abstract={Petri nets are widely recognized as a powerful model for discrete event systems. Petri nets have both graphical and mathematical features. Graphical feature provides an environment to design and to comprehend discrete event systems. Mathematical feature provides an analysis power for verifying several properties of such systems. Several analysis techniques have been proposed so far, such as a reachability (coverability) graph method, a matrix equation approach, reduction or decomposition techniques, a symbolic model method and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often used in the verification of asynchronous circuits. This paper focuses on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and a upper bound problem. Relations between these problems and an unfolding have been clarified to provide a novel method to resolve these problems.},
keywords={},
doi={},
ISSN={},
month={November},}
Copy
TY - JOUR
TI - A Graph Theoretic Approach to Reachability Problem with Petri Net Unfoldings
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1809
EP - 1816
AU - Toshiyuki MIYAMOTO
AU - Sadatoshi KUMAGAI
PY - 1996
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E79-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 1996
AB - Petri nets are widely recognized as a powerful model for discrete event systems. Petri nets have both graphical and mathematical features. Graphical feature provides an environment to design and to comprehend discrete event systems. Mathematical feature provides an analysis power for verifying several properties of such systems. Several analysis techniques have been proposed so far, such as a reachability (coverability) graph method, a matrix equation approach, reduction or decomposition techniques, a symbolic model method and an unfolding method. The unfolding method was introduced to avoid generating the reachability graph. Unfoldings are often used in the verification of asynchronous circuits. This paper focuses on an analysis of finite state systems, i.e., bounded nets, and discuss a reachability problem and a upper bound problem. Relations between these problems and an unfolding have been clarified to provide a novel method to resolve these problems.
ER -
English
