Selected publications at LSV: 2006

BHR06
Patricia Bouyer, Serge Haddad and Pierre-Alain Reynier.  Timed Unfoldings for Networks of Timed Automata.  In ATVA'06, LNCS 4218, pages 292-306. Springer, 2006. ( PDF | PS | PS.GZ )
doi: 10.1007/11901914_23
Abstract:
Whereas partial order methods have proved their efficiency for the analysis of discrete-event systems, their application to timed systems remains a challenging research topic. Here, we design a verification algorithm for networks of timed automata with invariants. Based on the unfolding technique, our method produces a branching process as an acyclic Petri net extended with read arcs. These arcs verify conditions on tokens without consuming them, thus expressing concurrency between conditions checks. They are useful for avoiding the explosion of the size of the unfolding due to clocks which are compared with constants but not reset. Furthermore, we attach zones to events, in addition to markings. We then compute a complete finite prefix of the unfolding. The presence of invariants goes against the concurrency since it entails a global synchronization on time. The use of read arcs and the analysis of the clock constraints appearing in invariants will help increasing the concurrency relation between events. Finally, the finite prefix we compute can be used to decide reachability properties, and transition enabling.

@inproceedings{BHR-atva06,
   address = {Beijing, China},
   author = {Bouyer, Patricia and Haddad, Serge and Reynier, Pierre-Alain},
   booktitle = {{P}roceedings of the 4th {I}nternational {S}ymposium on {A}utomated {T}echnology for {V}erification and {A}nalysis ({ATVA}'06)},
   DOI = {10.1007/11901914_23},
   editor = {Graf, Susanne and Zhang, Wenhui},
   month = oct,
   pages = {292-306},
   publisher = {Springer},
   series = {Lecture Notes in Computer Science},
   title = {Timed Unfoldings for Networks of Timed Automata},
   url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BHR-atva06.pdf},
   volume = {4218},
   year = {2006},
}

About LSV