Timed Unfoldings for Networks of Timed Automata
Bouyer, Patricia; Haddad, Serge; Reynier, Pierre-Alain (2006), Timed Unfoldings for Networks of Timed Automata, in Graf, Susanne; Zhang, Wenhui, Automated Technology for Verification and Analysis. 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006, Proceedings, Springer : Berlin, p. 292-306. http://dx.doi.org/10.1007/11901914_23
TypeCommunication / Conférence
Conference title4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006)
Book titleAutomated Technology for Verification and Analysis. 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006, Proceedings
Book authorGraf, Susanne; Zhang, Wenhui
Series titleLecture Notes in Computer Science
Number of pages540
MetadataShow full item record
Abstract (EN)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 ﬁnite 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 between events. Finally, the ﬁnite preﬁx can be used to decide reachability properties, and transition enabling.
Subjects / Keywordstimed automata; discrete-event systems; partial order methods; timed systems
Showing items related by title and author.