Model Checking of Time Petri Nets Using the State Class Timed Automaton

被引:0
作者
Didier Lime
Olivier H. Roux
机构
[1] CISS-Aalborg University,
[2] IRCCyN (Institut de Recherche en Communication et Cybernétique de Nantes),undefined
来源
Discrete Event Dynamic Systems | 2006年 / 16卷
关键词
Time petri nets; Timed automata; Model-checking; Dense-time systems;
D O I
暂无
中图分类号
学科分类号
摘要
In this paper, we propose a method for building the state class graph of a bounded time Petri net (TPN) as a timed automaton (TA), which we call the state class timed automaton. We consider bounded TPN, whose underlying net is not necessarily bounded. We prove that our translation preserves the behavioral semantics of the TPN (the initial TPN and the obtained TA are proved timed-bisimilar). It allows us to check real-time properties on TPN by using the state class TA. This can be done efficiently thanks to a reduction of the number of clocks. We have implemented the method, and give some experimental results illustrating the efficiency of the translation algorithm in terms of number of clocks. Using the state class TA, we also give a framework for expressing and efficiently verifying TCTL properties on the initial TPN.
引用
收藏
页码:179 / 205
页数:26
相关论文
共 22 条
[11]  
Henzinger TA(undefined)Kronos: a verification tool for real-time systems undefined undefined undefined-undefined
[12]  
Nicollin X(undefined)undefined undefined undefined undefined-undefined
[13]  
Sifakis J(undefined)undefined undefined undefined undefined-undefined
[14]  
Yovine S(undefined)undefined undefined undefined undefined-undefined
[15]  
Larsen KG(undefined)undefined undefined undefined undefined-undefined
[16]  
Pettersson P(undefined)undefined undefined undefined undefined-undefined
[17]  
Yi W(undefined)undefined undefined undefined undefined-undefined
[18]  
Popova L(undefined)undefined undefined undefined undefined-undefined
[19]  
Vicario E(undefined)undefined undefined undefined undefined-undefined
[20]  
Yoneda T(undefined)undefined undefined undefined undefined-undefined