Relevant Timed Schedules/Clock Vectors for Constructing Time Petri Net Reachability Graphs

被引：2

作者：

Boucheneb, Hanifa ^{[1
]}

Barkaoui, Kamel ^{[2
]}

机构：

[1] Ecole Polytech, Dept Comp Engn, Lab VeriForm, Montreal, PQ H3C 3A7, Canada

[2] Lab CEDRIC Conservatoire Natl Arts & Metiers, Paris 03, France

来源：

DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS | 2011年 / 21卷 / 02期

关键词：

Time Petri nets; Reachability graph; Timed schedule based graph; Clock vector based graph; TCTL MODEL CHECKING;

D O I：

10.1007/s10626-011-0100-4

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

We consider here the time Petri nets (the TPN model) and its state space abstractions. We show that only some timed schedules/clock vectors (one per enabled transition) of the clock/firing domains are relevant to construct reachability graphs for the TPN. Moreover, we prove formally that the resulting graphs are smaller than the TPN reachability graphs proposed in the literature. Furthermore, these results establish a relation between dense time and discrete time analysis of time Petri nets and allow also improving discrete time analysis by considering only some elements of the clock/firing domains.

引用

页码：171 / 204

页数：34

共 14 条

[1] Lower and upper bounds in zone-based abstractions of timed automata [J].

Gerd Behrmann ;

Patricia Bouyer ;

Kim G. Larsen ;

Radek Pelánek .

International Journal on Software Tools for Technology Transfer, 2006, 8 (3) :204-215

[2]

Bengtsson J., 2002, THESIS UPPSALA U

[3]

Berthomieu B, 2003, LECT NOTES COMPUT SC, V2619, P442

[4]

Berthomieu B., 2007, LNCS, V4762

[5] CTL* model checking for time Petri nets [J].

Boucheneb, H ;

Hadjidj, R .

THEORETICAL COMPUTER SCIENCE, 2006, 353 (1-3) :208-227

[6]

BOUCHENEB H, 2007, P 7 INT C APPL CONC, P61

[7] TCTL Model Checking of Time Petri Nets [J].

Boucheneb, Hanifa ;

Gardey, Guillaume ;

Roux, Olivier H. .

JOURNAL OF LOGIC AND COMPUTATION, 2009, 19 (06) :1509-1540

[8]

Cormen T.H., 2002, INTRO ALGORITHMS, V2nd

[9] State space computation and analysis of Time Petri Nets [J].

Gardey, Guillaume ;

Roux, Olivier H. ;

Roux, Olivier F. .

THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2006, 6 :301-320

[10] On-the-fly TCTL model checking for time Petri nets [J].

Hadjidj, Rachid ;

Boucheneb, Hanifa .

THEORETICAL COMPUTER SCIENCE, 2009, 410 (42) :4241-4261

← 1 2 →