A Graph Theoretic Approach to Reachability Problem with Petri Net Unfoldings

Toshiyuki MIYAMOTO; Sadatoshi KUMAGAI

A Graph Theoretic Approach to Reachability Problem with Petri Net Unfoldings

Toshiyuki MIYAMOTO, Sadatoshi KUMAGAI

Full Text Views

0

Share
Cite this

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

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://globals.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 -