2003 | OriginalPaper | Buchkapitel
Static Guard Analysis in Timed Automata Verification
verfasst von : Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim G. Larsen
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
By definitionTimedAutomata 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.