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

被引：0
作者：
Hanifa Boucheneb
Kamel Barkaoui
机构：
[1] École Polytechnique de Montréal,Laboratoire VeriForm, Department of Computer Engineering
[2] Conservatoire National des Arts et Métiers,Laboratoire CEDRIC
来源：
Discrete Event Dynamic Systems | 2011年 / 21卷
关键词：
Time Petri nets; Reachability graph; Timed schedule based graph; Clock vector based graph;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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
页数：33
相关论文
共 21 条
[1]  
Behrmann G(2006)Lower and upper bounds in zone-based abstractions of timed automata Int J Softw Tools Technol Transf 8 204-215
[2]  
Bouyer P(2003)State class constructions for branching analysis of time Petri nets LNCS 2619 442-457
[3]  
Larsen KG(2009)TCTL model checking of time Petri nets J Log Comput 19 1509-1540
[4]  
Pelànek R(2006)CTL* model checking for time Petri nets Journal of Theoretical Computer Science TCS 353 1-3
[5]  
Berthomieu B(2006)State space computation and analysis of time Petri nets Theory and Practice of Logic Programming (TPLP) 6 301-320
[6]  
Vernadat F(2009)On-the-fly TCTL model checking for time Petri nets Journal of Theoretical Computer Science TCS 410 4241-4261
[7]  
Boucheneb H(1999)Analyzing paths in time Petri nets Fundam Inform 37 311-327
[8]  
Gardey G(1998)Essential states in time Petri nets Informatik-Berichte 96 1-14
[9]  
Roux OH(1997)Efficient verification of parallel real-time systems Form Methods Syst Des 11 187-215
[10]  
Boucheneb H(undefined)undefined undefined undefined undefined-undefined
123