Also see
publications before 2005
(Show all abstracts)
(Hide all abstracts)
2009
-
Jan-Georg Smaus and Jörg Hoffmann.
Relaxation Refinement: A New Method to Generate Heuristic
Functions.
In
Doron Peled and Michael Wooldridge,
Proceedings of the 5th Workshop on Model Checking and Artificial Intelligence
(MoChArt 2008).
Springer-Verlag 2009.
(Show abstract)
(Hide abstract)
(PDF)
(BIB)
In artificial intelligence, a relaxation of a problem
is an overapproximation whose solution in every state of an
explicit search provides a heuristic solution distance estimate.
The heuristic guides the exploration, potentially shortening the
search by exponentially many search states. The big question is
how a good relaxation for the problem at hand should be derived.
In model checking, overapproximations are called
abstractions, and abstraction refinement is a
powerful method developed to derive approximations that are
sufficiently precise for verifying the system at hand.
In our work, we bring these two paradigms together. We pioneer
the application of (predicate) abstraction refinement for the
generation of heuristic functions that are intelligently adapted
to the problem at hand. We investigate how an abstraction
refinement process for generating heuristic functions should
differ from the process used in the verification context. We do
so in the context of DMC of timed automata. We obtain a variety
of interesting insights about this approach.
2007
-
Jan-Georg Smaus.
On Boolean Functions Encodable as a Single Linear Pseudo-Boolean
Constraint.
In
Pascal Van Hentenryck and Laurence Wolsey,
Proceedings of the 4th International Conference on
Integration of AI and OR Techniques in Constraint Programming
for Combinatorial Optimization Problems (CPAIOR 2007), pp. 288-302.
Springer 2007.
(PDF)
2006
-
Jan-Georg Smaus.
Representing Boolean Functions as Linear Pseudo-Boolean
Constraints.
In
CP 2006 Workshop on the
Integration of SAT and CP techniques.
2006.
-
Jörg Hoffmann, Jan-Georg Smaus, Andrey Rybalchenko, Sebastian Kupferschmid and Andreas Podelski.
Using Predicate Abstraction to Generate Heuristic Functions in
Uppaal.
In
Stefan Edelkamp and Alessio Lomuscio,
Proceedings of the 4th Workshop on Model Checking and Artificial Intelligence
(MoChArt 2006), pp. 51-66.
Springer-Verlag 2006.
(Show abstract)
(Hide abstract)
(PDF)
(BIB)
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.
-
Stefan Ratschan and Jan-Georg Smaus.
Verification-Integrated Falsification of Non-deterministic Hybrid
Systems.
In
Proceedings of the 2nd IFAC Conference on Analysis and Design of
Hybrid Systems (ADHS
2006).
2006.
2004
