Efficient Reachability Analysis for Time Petri Nets

被引：34

作者：

Hadjidj, Rachid ^{[1
]}

Boucheneb, Hanifa ^{[2
]}

机构：

[1] Qatar Univ, Dept Comp Sci & Engn, Doha, Qatar

[2] Ecole Polytech, Dept Comp Engn, Stn Centreville, Montreal, PQ H3C 3A7, Canada

来源：

IEEE TRANSACTIONS ON COMPUTERS | 2011年 / 60卷 / 08期

基金：

加拿大自然科学与工程研究理事会;

关键词：

Formal methods; time Petri nets (TPN); state class spaces; reachability properties; model checking;

D O I：

10.1109/TC.2010.195

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

080201 [机械制造及其自动化];

摘要：

We propose in this paper some efficient approaches, based on the state class graph method, to construct abstractions for the Time Petri Net (TPN) model, suitable to verify its linear or reachability properties. Experimental results have shown that these abstractions are very appropriate as both time and size are considerably reduced. For some tested models, abstractions that preserve reachability properties can be as many as 2,051 times smaller and more than 592 times faster to compute. For abstractions, which are overapproximations (useful to prove that certain states are not reachable), gains can overpass 10,000 for both time and size.

引用

页码：1085 / 1099

页数：15

共 27 条

[1]

A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2]

Approximate reachability analysis of timed automata [J].

Balarin, F .

17TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1996, :52-61

[3]

Behrmann G., 2002, Formal Techniques in Real-Time and Fault-Tolerant Systems. 7th International Symposium, FTRTFT 2002. Proceedings (Lecture Notes in Computer Science Vol.2469), P3

[4]

DYNAMIC PROGRAMMING [J].