CTL Model Checking of Time Petri Nets Using Geometric Regions
Summary :
Geometric region method is one of the techniques to handle real-time systems which have potentially infinite state spaces. However, the original geometric region method gives incorrect results for the CTL model checking of time Petri nets. In this paper, we discuss the sufficient condition for the geometric region graphs to be correct with respect to the CTL model checking of time Petri nets, and then propose a technique to partition given geometric regions so that the graphs satisfy the sufficient condition. Finally, we implement the proposed algorithm, and compare it with the other methods by using small examples.
- Publication
- IEICE TRANSACTIONS on Information Vol.E81-D No.3 pp.297-306
- Publication Date
- 1998/03/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- Category
- Fault Tolerant Computing
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
Tomohiro YONEDA, Hikaru RYUBA, "CTL Model Checking of Time Petri Nets Using Geometric Regions" in IEICE TRANSACTIONS on Information,
vol. E81-D, no. 3, pp. 297-306, March 1998, doi: .
Abstract: Geometric region method is one of the techniques to handle real-time systems which have potentially infinite state spaces. However, the original geometric region method gives incorrect results for the CTL model checking of time Petri nets. In this paper, we discuss the sufficient condition for the geometric region graphs to be correct with respect to the CTL model checking of time Petri nets, and then propose a technique to partition given geometric regions so that the graphs satisfy the sufficient condition. Finally, we implement the proposed algorithm, and compare it with the other methods by using small examples.
URL: https://global.ieice.org/en_transactions/information/10.1587/e81-d_3_297/_p
Copy
@ARTICLE{e81-d_3_297,
author={Tomohiro YONEDA, Hikaru RYUBA, },
journal={IEICE TRANSACTIONS on Information},
title={CTL Model Checking of Time Petri Nets Using Geometric Regions},
year={1998},
volume={E81-D},
number={3},
pages={297-306},
abstract={Geometric region method is one of the techniques to handle real-time systems which have potentially infinite state spaces. However, the original geometric region method gives incorrect results for the CTL model checking of time Petri nets. In this paper, we discuss the sufficient condition for the geometric region graphs to be correct with respect to the CTL model checking of time Petri nets, and then propose a technique to partition given geometric regions so that the graphs satisfy the sufficient condition. Finally, we implement the proposed algorithm, and compare it with the other methods by using small examples.},
keywords={},
doi={},
ISSN={},
month={March},}
Copy
TY - JOUR
TI - CTL Model Checking of Time Petri Nets Using Geometric Regions
T2 - IEICE TRANSACTIONS on Information
SP - 297
EP - 306
AU - Tomohiro YONEDA
AU - Hikaru RYUBA
PY - 1998
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E81-D
IS - 3
JA - IEICE TRANSACTIONS on Information
Y1 - March 1998
AB - Geometric region method is one of the techniques to handle real-time systems which have potentially infinite state spaces. However, the original geometric region method gives incorrect results for the CTL model checking of time Petri nets. In this paper, we discuss the sufficient condition for the geometric region graphs to be correct with respect to the CTL model checking of time Petri nets, and then propose a technique to partition given geometric regions so that the graphs satisfy the sufficient condition. Finally, we implement the proposed algorithm, and compare it with the other methods by using small examples.
ER -
English
