IEICE TRANSACTIONS on Fundamentals
Reduction Operators Based on Behavioral Inheritance for Timed Petri Nets
Summary :
In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E97-A No.2 pp.484-489
- Publication Date
- 2014/02/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1587/transfun.E97.A.484
- Type of Manuscript
- Special Section LETTER (Special Section on Mathematical Systems Science and its Applications)
- Category
Authors
Ichiro TOYOSHIMA
Yamaguchi University
Shota NAKANO
Yamaguchi University
Shingo YAMAGUCHI
Yamaguchi University
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
Ichiro TOYOSHIMA, Shota NAKANO, Shingo YAMAGUCHI, "Reduction Operators Based on Behavioral Inheritance for Timed Petri Nets" in IEICE TRANSACTIONS on Fundamentals,
vol. E97-A, no. 2, pp. 484-489, February 2014, doi: 10.1587/transfun.E97.A.484.
Abstract: In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E97.A.484/_p
Copy
@ARTICLE{e97-a_2_484,
author={Ichiro TOYOSHIMA, Shota NAKANO, Shingo YAMAGUCHI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Reduction Operators Based on Behavioral Inheritance for Timed Petri Nets},
year={2014},
volume={E97-A},
number={2},
pages={484-489},
abstract={In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.},
keywords={},
doi={10.1587/transfun.E97.A.484},
ISSN={1745-1337},
month={February},}
Copy
TY - JOUR
TI - Reduction Operators Based on Behavioral Inheritance for Timed Petri Nets
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 484
EP - 489
AU - Ichiro TOYOSHIMA
AU - Shota NAKANO
AU - Shingo YAMAGUCHI
PY - 2014
DO - 10.1587/transfun.E97.A.484
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E97-A
IS - 2
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - February 2014
AB - In this paper, we proposed reduction operators of timed Petri net for efficient model checking. Timed Petri nets are used widely for modeling and analyzing systems which include time concept. Analysis of the system can be done comprehensively with model checking, but there is a state-space explosion problem. Therefore, previous researchers proposed reduction methods and translation methods to timed automata to perform efficient model checking. However, there is no reduction method which consider observability and there is a trade-off between the amount of description and the size of state space. In this paper, first, we have defined a concept of timed behavioral inheritance. Next, we have proposed reduction operators of timed Petri nets based on timed behavioral inheritance. Then, we have applied our proposed operators to an artificial timed Petri net. Moreover, the results show that the reduction operators which consider observability can reduce the size of state space of the original timed Petri nets within the experiment.
ER -
English
