Static guard analysis in timed automata verification. In Tools and Algorithms for the Construction and Analysis of Systems

Abstract. By definition Timed Automata have an infinite state-space, thus for verification purposes, an exact finite abstraction is required. We propose a location-based finite zone abstraction, which computes an abstraction based on the rele-vant 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 expo-nential speedup compared to the usual abstraction.