Timed Unfoldings for Networks of Timed Automata

13 years 10 months ago
Timed Unfoldings for Networks of Timed Automata
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 helps increasing the concurrency relation...
Patricia Bouyer, Serge Haddad, Pierre-Alain Reynie
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Patricia Bouyer, Serge Haddad, Pierre-Alain Reynier
Comments (0)