Paper Info
Title
A New Approach to Abstract Reachability State Space of Time Petri Nets
Abstract
Time Petri nets (TPN model) allow the specification of real-time systems involving explicit timing constraints. The main challenge of the analysis of such systems is to construct, with few resources (time and space), a coarse abstraction preserving timed properties. In this paper, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behaviour of bounded TPNs with strong time semantics. The main feature of this abstract representation compared to existing approaches is the encoding of the time information. This is done in a pure way within each node of the TAG allowing to compute the minimum and maximum elapsed time in every path of the graph. The TAG preserves runs and reachable states of the corresponding TPN and allows for verification of both event- and state-based properties.
Year
DOI
Venue
2013
10.1109/TIME.2013.22
TIME
Keywords
Field
DocType
strong time semantics,model checking of timed properties,tpn model,petri nets,tag,time petri nets,corresponding tpn,event-based properties,state-based properties,time petri net,time information,real time systems,main feature,abstract reachability state space,timed aggregate graph,new approach,new finite graph,main challenge,real-time systems,state space abstraction,formal specification,abstract representation,reachability analysis
Petri net,Computer science,Formal specification,Process architecture,Reachability,Theoretical computer science,Stochastic Petri net,State space,Bounded function,Encoding (memory)
Conference
ISSN
ISBN
Citations 
1530-1311
978-1-4799-2240-6
2
PageRank 
References 
Authors
0.38
12
3
Name
Order
Citations
PageRank
Kaïs Klai125927.20
Naim Aber2120.93
Laure Petrucci352151.44