By definition Timed Automata have an infinite state-space, thus for verification purposes, an exact finite abstraction is required. We propose a locationbased finite zone abstraction, which computes an abstraction based on the relevant guards for a particular state of the model (as opposed to all guards). We show that the location-based zone abstraction is sound and complete with respect to location reachability; that it generalises active-clock reduction, in the sense that an inactive clock has no relevant guards at all; that it enlarges the class of timed automata, that can be verified. We generalise the new abstraction to the case of networks of timed automata, and experimentally demonstrate a potentially exponential speedup compared to the usual abstraction. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Behrmann, G., Bouyer, P., Fleury, E., & Larsen, K. G. (2003). Static guard analysis in timed automata verification. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2619, 254–270. https://doi.org/10.1007/3-540-36577-x_18
Mendeley helps you to discover research relevant for your work.