Using Predicate Abstraction to Generate Heuristic
Functions in Uppaal
Abstract
We focus on checking safety properties in networks of extended timed
automata, with the well-known UPPAAL system. We show how to use
predicate abstraction, in the sense used in model checking, to
generate search guidance, in the sense used in Artificial
Intelligence (AI). This contributes another family of heuristic
functions to the growing body of work on directed model
checking. The overall methodology follows the pattern
database approach from AI: the abstract state space is
exhaustively built in a pre-process, and used as a lookup table
during search. While typically pattern databases use rather
primitive abstractions ignoring some of the relevant symbols, we use
predicate abstraction, dividing the state space into
equivalence classes with respect to a list of logical expressions
(predicates). We empirically explore the behavior of the resulting
family of heuristics, in a meaningful set of benchmarks. In
particular, while several challenges remain open, we show that one
can easily obtain heuristic functions that are competitive with the
state-of-the-art in directed model checking.
Jan-Georg Smaus
Last modified: Thu Mar 1 16:56:39 MET 2007