2006 | OriginalPaper | Buchkapitel
Adapting an AI Planning Heuristic for Directed Model Checking
verfasst von : Sebastian Kupferschmid, Jörg Hoffmann, Henning Dierks, Gerd Behrmann
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
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
There is a growing body of work on directed model checking, which improves the falsification of safety properties by providing heuristic functions that can guide the search
quickly
towards
short
error paths. Techniques of this kind have also been made very successful in the area of AI Planning. Our main technical contribution is the adaptation of the most successful heuristic function from AI Planning to the model checking context, yielding a new heuristic for directed model checking. The heuristic is based on solving an abstracted problem in every search state. We adapt the abstraction and its solution to networks of communicating automata annotated with (constraints and effects on) integer variables. Since our ultimate goal in this research is to also take into account clock variables, as used in timed automata, our techniques are implemented inside UPPAAL. We run experiments in some toy benchmarks for timed automata, and in two timed automata case studies originating from an industrial project. Compared to both blind search and some previously proposed heuristic functions, we consistently obtain significant, sometimes dramatic, search space reductions, resulting in likewise strong reductions of runtime and memory requirements.