loading...
Much Compact Time Petri Net State Class Spaces Useful to Restore CTL* Properties
St. Malo, France June 07-June 09
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ACSD.2005.28Fifth International Conference on App ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Rachid Hadjidj, ?col? Polytechnique de Montr?al
Hanifa Boucheneb, ?cole Polytechnique de Montr?al
This paper deals with the verification of CTL* properties of Time Petri Nets (TPN model). To verify such properties, we need to contract the generally infinite state space of the TPN model into a finite graph that preserves its CTL* properties. Such a graph can be constructed using a partition refinement technique, where an intermediate graph, representing a contraction of the TPN state space, is first built then refined until CTL* properties are restored. Comparing to other approaches, we propose to construct much compact intermediate graphs. Experimental results have shown that our contractions are very appropriate to boost the refinement procedure. We have been able to reduce computation times by factors reaching four and more in certain cases. Resulting graphs have also been reduced in size.
Citation:
Rachid Hadjidj, Hanifa Boucheneb, "Much Compact Time Petri Net State Class Spaces Useful to Restore CTL* Properties," acsd, pp.224-233, Fifth International Conference on Application of Concurrency to System Design (ACSD'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.