Diese Seite ist nur auf Englisch verfügbar.

Prof. Jan-Georg Smaus – Publikationen

Also see publications before 2005

(Show all abstracts) (Hide all abstracts)

2009

Bahareh Badban, Stefan Leue and Jan-Georg Smaus.
Automated Predicate Abstraction for Real-Time Models.
In Axel Legay and Azadeh Farzan (ed.), Proceedings of the 11th International Workshop on Verification of Infinite-State Systems (INFINITY 2009), pp. 36-43. 2009.
(Show abstract) (Hide abstract) (PDF) (BIB)

We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We use the CIPM algorithm in our previous work which computes new invariants for timed automata control locations and prunes the model, to compute a predicate abstraction of the model. We do so by taking information regarding control locations and their newly computed invariants into account.
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 (ed.), 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 (ed.), 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 (ed.), 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 (eds.), 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 (ed.), 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 (eds.), 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 (eds.), 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

Jan-Georg Smaus.
Termination of Logic Programs Using Various Dynamic Selection Rules.
In Proceedings of the 20th International Conference on Logic Programming (ICLP'04). 2004.
(PS.GZ) (PDF)