非表示:
キーワード:
-
要旨:
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.
This work was partly supported by the German Research Council (DFG) as part of
the Transregional Collaborative Research Center “Automatic Verification and
Analysis of Complex Systems” (SFB/TR 14 AVACS). See http://www.avacs.org/ for
more information.
