loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Seventh International Conference on Application of Concurrency to System Design (ACSD 2007)
A more efficient time Petri net state space abstraction preserving linear properties
Bratislava, Slovak Republic
July 10-July 13
ISBN: 0-7695-2902-X
Hanifa Boucheneb, Ecole Polytechnique de Montreal, Canada
Hind Rakkay, Ecole Polytechnique de Montreal, Canada
We consider here Time Petri nets (TPN model). We first propose an abstraction to its generally infinite state space which preserves linear properties1 of the TPN model. Comparing with TPN abstractions proposed in the literature, our abstraction produces graphs which are both smaller and faster to compute. In addition, our characterization of abstracted states allows a significative gain in space. Afterwards, we show how to apply Yoneda?s partial order reduction technique to construct directly reduced graphs useful to verify LTL-X properties of the model. Using our approach, both time and space complexities are significantly reduced.
Index Terms:
Time Petri nets, state class graph, state explosion problem, partial order techniques, independent transitions, relevant execution path.
Citation:
Hanifa Boucheneb, Hind Rakkay, "A more efficient time Petri net state space abstraction preserving linear properties," acsd, pp.61-70, Seventh International Conference on Application of Concurrency to System Design (ACSD 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.