|
|
Dr. Jan-Georg Smaus – Publikationen
Also see
publications before 2005
(Show all abstracts)
(Hide all abstracts)
2009
-
Stefan Ratschan and Jan-Georg Smaus.
Finding Errors of Hybrid Systems by Optimising
an Abstraction-Based Quality Estimate.
Technical Report 51,
SFB/TR 14 AVACS, 2009.
(Show abstract)
(Hide abstract)
(PDF)
(BIB)
We present an algorithm for falsifying safety properties of hybrid
systems, i.e., for finding a trajectory to an unsafe state. The
approach is to approximate how close a point is to being an initial
point of an error trajectory using a real-valued quality function, and
then to use numerical optimisation to search for an optimum of this
function. The function is computed by running simulations, where
information coming from abstractions computed by a verification
algorithm is exploited to determine whether a simulation looks
promising and should be continued or cancelled. This information
becomes more reliable as the abstraction becomes more refined. We thus
interleave falsification and verification attempts.
-
Alexander Schimpf, Stephan Merz and Jan-Georg Smaus.
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL.
In
Stefan Berghofer and Tobias Nipkow and Christian
Urban and Makarius Wenzel,
Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics
(TPHOLs 2009), pp. 424-439.
Springer-Verlag 2009.
(Show abstract)
(Hide abstract)
(BIB)
We present the implementation of a translation of LTL formulae into
automata in Isabelle/HOL, which is an essential component of LTL
model checking algorithms. In automaton-based model checking, we
have a system modelled as a transition system and a correctness
property stated as a temporal (in our case: LTL) formula.
Such a formula can be translated into a (generalised) Büchi
automaton that accepts precisely those behaviours allowed by the
formula. Checking correctness of the system thus amounts to a
language inclusion property between the two automata. We implemented
a standard translation algorithm due to Gerth et al. The
correctness and termination of our implementation is shown in
Isabelle/HOL, and executable code is generated using the
Isabelle/HOL code generator.
-
Stefan Ratschan and Jan-Georg Smaus.
Finding Errors of Hybrid Systems by Optimising
an Abstraction-Based Quality Estimate.
In
Catherine Dubois,
Proceedings of the 3rd International Conference on Tests And Proofs
(TAP 2009), pp. 153-168.
Springer-Verlag 2009.
(Show abstract)
(Hide abstract)
(PDF)
(BIB)
We present an algorithm for falsifying safety properties of hybrid
systems, i.e., for finding a trajectory to an unsafe state. The
approach is to approximate how close a point is to being an initial
point of an error trajectory using a real-valued quality function, and
then to use numerical optimisation to search for an optimum of this
function. The function is computed by running simulations, where
information coming from abstractions computed by a verification
algorithm is exploited to determine whether a simulation looks
promising and should be continued or cancelled. This information
becomes more reliable as the abstraction becomes more refined. We thus
interleave falsification and verification attempts.
-
Bahareh Badban, Stefan Leue and Jan-Georg Smaus.
Automated Invariant Generation for the Verification
of Real-Time Systems.
In
Andrew Ireland and Laura Kovács,
Proceedings of the 2nd International Workshop on
Invariant Generation
(WING 2009).
2009.
(Show abstract)
(Hide abstract)
(PDF)
(BIB)
We present an approach to automatically generating invariants for timed automata
models. The CIPM algorithm that we propose first computes new invariants
for timed automata control locations taking their originally defined invariants
as well as the constrains on clock variables
imposed by incoming state transitions into account. In doing
so the CIPM algorithm also prunes idle transitions, which are transitions that can never
be taken, from the automaton. We discsuss a prototype implementation of the
CIPM algorithm as well as some initial experimental results.
-
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), pp. 147-165.
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.
2008
-
Stefan Ratschan and Jan-Georg Smaus.
Finding Errors of Hybrid Systems by Optimising
an Abstraction-Based Quality Estimate.
In
Tarmo Uustalu and Jüri Vain,
Proceedings of the 20th Nordic Workshop on Programming Theory
(NWPT 2008), pp. 72-74.
2008.
(PDF)
(BIB)
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
|
