IEICE TRANSACTIONS on Fundamentals
An Efficient Translation Method from Timed Petri Nets to Timed Automata
Summary :
There are various existing methods translating timed Petri nets to timed automata. However, there is a trade-off between the amount of description and the size of state space. The amount of description and the size of state space affect the feasibility of modeling and analysis like model checking. In this paper, we propose a new translation method from timed Petri nets to timed automata. Our method translates from a timed Petri net to an automaton with the following features: (i) The number of location is 1; (ii) Each edge represents the firing of transition; (iii) Each state implemented as clocks and variables represents a state of the timed Petri net one-to-one correspondingly. Through these features, the amount of description is linear order and the size of state space is the same order as that of the Petri net. We applied our method to three Petri net models of signaling pathways and compared our method with existing methods from the view points of the amount of description and the size of state space. And the comparison results show that our method keeps a good balance between the amount of description and the size of state space. These results also show that our method is effective when checking properties of timed Petri nets.
- Publication
- IEICE TRANSACTIONS on Fundamentals Vol.E95-A No.8 pp.1402-1411
- Publication Date
- 2012/08/01
- Publicized
- Online ISSN
- 1745-1337
- DOI
- 10.1587/transfun.E95.A.1402
- Type of Manuscript
- PAPER
- Category
- Concurrent Systems
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
Shota NAKANO, Shingo YAMAGUCHI, "An Efficient Translation Method from Timed Petri Nets to Timed Automata" in IEICE TRANSACTIONS on Fundamentals,
vol. E95-A, no. 8, pp. 1402-1411, August 2012, doi: 10.1587/transfun.E95.A.1402.
Abstract: There are various existing methods translating timed Petri nets to timed automata. However, there is a trade-off between the amount of description and the size of state space. The amount of description and the size of state space affect the feasibility of modeling and analysis like model checking. In this paper, we propose a new translation method from timed Petri nets to timed automata. Our method translates from a timed Petri net to an automaton with the following features: (i) The number of location is 1; (ii) Each edge represents the firing of transition; (iii) Each state implemented as clocks and variables represents a state of the timed Petri net one-to-one correspondingly. Through these features, the amount of description is linear order and the size of state space is the same order as that of the Petri net. We applied our method to three Petri net models of signaling pathways and compared our method with existing methods from the view points of the amount of description and the size of state space. And the comparison results show that our method keeps a good balance between the amount of description and the size of state space. These results also show that our method is effective when checking properties of timed Petri nets.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/transfun.E95.A.1402/_p
Copy
@ARTICLE{e95-a_8_1402,
author={Shota NAKANO, Shingo YAMAGUCHI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={An Efficient Translation Method from Timed Petri Nets to Timed Automata},
year={2012},
volume={E95-A},
number={8},
pages={1402-1411},
abstract={There are various existing methods translating timed Petri nets to timed automata. However, there is a trade-off between the amount of description and the size of state space. The amount of description and the size of state space affect the feasibility of modeling and analysis like model checking. In this paper, we propose a new translation method from timed Petri nets to timed automata. Our method translates from a timed Petri net to an automaton with the following features: (i) The number of location is 1; (ii) Each edge represents the firing of transition; (iii) Each state implemented as clocks and variables represents a state of the timed Petri net one-to-one correspondingly. Through these features, the amount of description is linear order and the size of state space is the same order as that of the Petri net. We applied our method to three Petri net models of signaling pathways and compared our method with existing methods from the view points of the amount of description and the size of state space. And the comparison results show that our method keeps a good balance between the amount of description and the size of state space. These results also show that our method is effective when checking properties of timed Petri nets.},
keywords={},
doi={10.1587/transfun.E95.A.1402},
ISSN={1745-1337},
month={August},}
Copy
TY - JOUR
TI - An Efficient Translation Method from Timed Petri Nets to Timed Automata
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 1402
EP - 1411
AU - Shota NAKANO
AU - Shingo YAMAGUCHI
PY - 2012
DO - 10.1587/transfun.E95.A.1402
JO - IEICE TRANSACTIONS on Fundamentals
SN - 1745-1337
VL - E95-A
IS - 8
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - August 2012
AB - There are various existing methods translating timed Petri nets to timed automata. However, there is a trade-off between the amount of description and the size of state space. The amount of description and the size of state space affect the feasibility of modeling and analysis like model checking. In this paper, we propose a new translation method from timed Petri nets to timed automata. Our method translates from a timed Petri net to an automaton with the following features: (i) The number of location is 1; (ii) Each edge represents the firing of transition; (iii) Each state implemented as clocks and variables represents a state of the timed Petri net one-to-one correspondingly. Through these features, the amount of description is linear order and the size of state space is the same order as that of the Petri net. We applied our method to three Petri net models of signaling pathways and compared our method with existing methods from the view points of the amount of description and the size of state space. And the comparison results show that our method keeps a good balance between the amount of description and the size of state space. These results also show that our method is effective when checking properties of timed Petri nets.
ER -
English
