Sebastian Kupferschmid – Publications

(Show all abstracts) (Hide all abstracts)

2011

Sebastian Kupferschmid and Martin Wehrle.
Abstractions and Pattern Databases: The Quest for Succinctness and Accuracy.
In Parosh A. Abdulla and K. Rustan M. Leino (ed.), Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2011), pp. 276-290. Springer-Verlag 2011.
(Show abstract) (Hide abstract) (PDF) (BIB)

Directed model checking is a well-established technique for detecting error states in concurrent systems efficiently. As error traces are important for debugging purposes, it is preferable to find as short error traces as possible. A wide spread method to find provably shortest error traces is to apply the A* search algorithm with distance heuristics that never overestimate the real error distance. An important class of such distance estimators is the class of pattern database heuristics, which are built on abstractions of the system under consideration. In this paper, we propose a systematic approach for the construction of pattern database heuristics. We formally define a concept to measure the accuracy of abstractions. Based on this technique, we address the challenge of finding abstractions that are succinct on the one hand, and accurate to produce informed pattern databases on the other hand. We evaluate our approach on large and complex industrial problems. The experiments show that the resulting distance heuristic impressively advances the state of the art.

2010

Martin Wehrle and Sebastian Kupferschmid.
Context-Enhanced Directed Model Checking.
In Jaco van de Pol and Michael Weber (eds.), Proceedings of the 17th International SPIN Workshop on Model Checking Software (SPIN 2010), pp. 88-105. Springer-Verlag 2010.
(Show abstract) (Hide abstract) (PDF) (BIB)

Directed model checking is a well-established technique to efficiently tackle the state explosion problem when the aim is to find error states in concurrent systems. Although directed model checking has proved to be very successful in the past, additional search techniques provide much potential to efficiently handle larger and larger systems. In this work, we propose a novel technique for traversing the state space based on interference contexts. The basic idea is to preferably explore transitions that interfere with previously applied transitions, whereas other transitions are deferred accordingly. Our approach is orthogonal to the model checking process and can be applied to a wide range of search methods. We have implemented our method and empirically evaluated its potential on a range of non-trivial case studies. Compared to standard model checking techniques, we are able to detect subtle bugs with shorter error traces, consuming less memory and time.

2009

Sebastian Kupferschmid.
Directed Model Checking for Timed Automata.
Dissertation, Albert-Ludwigs-Universität, Freiburg, Germany 2009.
(BIB) (PDF) (FreiDok)
Martin Wehrle, Sebastian Kupferschmid and Andreas Podelski.
Transition-based Directed Model Checking.
In Stefan Kowalewski and Anna Philippou (eds.), Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), pp. 186-200. Springer-Verlag 2009.
(Show abstract) (Hide abstract) (PDF) (BIB)

Directed model checking is a well-established technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by influencing the order in which states are explored during the state space traversal. The order is typically determined by an abstract distance function that estimates a state's distance to a nearest error state. In this paper, we propose a general enhancement to directed model checking based on the evaluation of state transitions. We present a schema, parametrized by an abstract distance function, to evaluate transitions and propose a new method for the state space traversal. Our framework can be applied automatically to a wide range of abstract distance functions. The empirical evaluation impressively shows its practical potential. Apparently, the new method identifies a sweet spot in the trade-off between scalability (memory consumption) and short error traces.

2008

Thomas Keller and Sebastian Kupferschmid.
Automatic Bidding for the Game of Skat.
In Andreas R. Dengel, Karsten Berns, Thomas M. Breuel, Frank Bomarius and Thomas R. Roth-Berghofer (eds.), Proceedings of the 31st Annual German Conference on Artificial Intelligence (KI 2008), pp. 95-102. Springer-Verlag 2008.
(Show abstract) (Hide abstract) (BIB) (PDF)

In recent years, researchers started to study the game of Skat. The strength of existing Skat playing programs is definitely the card play phase. The bidding phase, however, was treated quite poorly so far. This is a severe drawback since bidding abilities influence the overall playing performance drastically. In this paper we present a powerful bidding engine which is based on a k-nearest neighbor algorithm.
Martin Wehrle, Sebastian Kupferschmid and Andreas Podelski.
Useless Actions are Useful.
In Jussi Rintanen, Bernhard Nebel, J. Christopher Beck and Eric Hansen (eds.), Proceedings of the 18th International Conference on Automated Planning and Scheduling (ICAPS 2008), pp. 388-395. AAAI Press 2008.
(Show abstract) (Hide abstract) (PDF) (BIB)

Planning as heuristic search is a powerful approach to solving domain independent planning problems. In recent years, various successful heuristics and planners like FF, LPG, Fast Downward or SGPlan have been proposed in this context. However, as heuristics only estimate the distance to goal states, a general problem of heuristic search is the existence of plateaus in the search space topology which can cause the search process to degenerate. Additional techniques like helpful actions or preferred operators that evaluate the "usefulness" of actions are often successful strategies to support the search in such situations.

In this paper, we introduce a general method to evaluate the usefulness of actions. We propose a technique to enhance heuristic search by identifying "useless" actions that are not needed to find optimal plans. In contrast to helpful actions or preferred operators that are specific to the FF and Causal Graph heuristic, respectively, our method can be combined with arbitrary heuristics. We show that this technique often yields significant performance improvements.
Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel and Andreas Podelski.
Faster than Uppaal?
In A. Gupta and S. Malik (eds.), Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), pp. 552-555. Springer-Verlag 2008.
(Show abstract) (Hide abstract) (PDF) (BIB)

It is probably very hard to develop a new model checker that is faster than Uppaal for verifying correct timed automata. In fact, our tool Mcta does not even try to compete with Uppaal in this (i.e., Uppaal's) arena. Instead, Mcta is geared towards analyzing incorrect specifications of timed automata. It returns (shorter) error traces faster.
Sebastian Kupferschmid, Jörg Hoffmann and Kim G. Larsen.
Fast Directed Model Checking via Russian Doll Abstraction.
In C. R. Ramakrishnan and J. Rehof (eds.), Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), pp. 203-217. Springer-Verlag 2008.
(Show abstract) (Hide abstract) (PDF) (BIB)

Directed model checking aims at speeding up the search for bugs in a system through the use of heuristic functions. Such a function maps states to integers, estimating the state's distance to the nearest error state. The search gives a preference to states with lower estimates. The key issue is how to generate good heuristic functions, i.e., functions that guide the search quickly to an error state. An arsenal of heuristic functions has been developed in recent years. Significant progress was made, but many problems still prove to be notoriously hard. In particular, a body of work describes heuristic functions for model checking timed automata in Uppaal, and tested them on a certain set of benchmarks. Into this arsenal we add another heuristic function. With previous heuristics, for the largest of the benchmarks it was only just possible to find some (unnecessarily long) error path. With the new heuristic, we can find provably shortest error paths for these benchmarks in a matter of seconds. The heuristic function is based on a kind of Russian Doll principle, where the heuristic for a given problem arises through using Uppaal itself for the complete exploration of a simplified instance of the same problem. The simplification consists in removing those parts from the problem that are distant from the error property. As our empirical results confirm, this simplification often preserves the characteristic structure leading to the error.

2007

Henning Dierks, Sebastian Kupferschmid and Kim G. Larsen.
Automatic Abstraction Refinement for Timed Automata.
In Jean-François Raskin and P. S. Thiagarajan (eds.), Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2007), pp. 114-129. Springer-Verlag 2007.
(Show abstract) (Hide abstract) (PDF) (BIB)

We present a fully automatic approach for counterexample guided abstraction refinement of real-time systems modelled in a subset of timed automata. Our approach is implemented in the Moby/RT tool environment, which is a CASE tool for embedded system specifications. Verification in Moby/RT is done by constructing abstractions of the semantics in terms of timed automata which are fed into the model checker Uppaal. Since the abstractions are over-approximations, absence of abstract counterexamples implies a valid result for the full model. Our new approach deals with the situation in which an abstract counterexample is found by Uppaal. The generated abstract counterexample is used to construct either a concrete counterexample for the full model or to identify a slightly refined abstraction in which the found spurious counterexample cannot occur anymore. Hence, the approach allows for a fully automatic abstraction refinement loop starting from the coarsest abstraction towards an abstraction for which a valid verification result is found. Nontrivial case studies demonstrate that this approach computes small abstractions fast without any user interaction.
Sebastian Kupferschmid, Klaus Dräger, Jörg Hoffmann, Bernd Finkbeiner, Henning Dierks, Andreas Podelski and Gerd Behrmann.
UPPAAL/DMC - Abstraction-based Heuristics for Directed Model Checking.
In Orna Grumberg and Michael Huth (eds.), Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), pp. 679-682. Springer-Verlag 2007.
(Show abstract) (Hide abstract) (PDF) (BIB)

Uppaal/DMC is an extension of Uppaal that provides generic heuristics for directed model checking. In this approach, the traversal of the state space is guided by a heuristic function which estimates the distance of a search state to the nearest error state. Our tool combines two recent approaches to design such estimation functions. Both are based on computing an abstraction of the system and using the error distance in this abstraction as the heuristic value. The abstractions, and thus the heuristic functions, are generated fully automatically and do not need any additional user input. Uppaal/DMC needs less time and memory to find shorter error paths than Uppaal's standard search methods.

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.
Sebastian Kupferschmid and Malte Helmert.
A Skat Player Based on Monte Carlo Simulation.
In H. Jaap van den Herik, Paolo Ciancarini and H. H. L. M. Donkers (eds.), Proceedings of the Fifth International Conference on Computer and Games (CG 2006), pp. 135-147. Springer-Verlag 2006.
(Show abstract) (Hide abstract) (PDF) (BIB)

We apply Monte Carlo simulation and alpha-beta search to the card game of Skat, which is similar to Bridge, but different enough to require some new algorithmic ideas besides the techniques developed for Bridge. Our Skat-playing program integrates well-known techniques such as move ordering with two new search enhancements. Quasi-symmetry reduction generalizes symmetry reductions, popularized by Ginsberg's Partition Search algorithm, to search states which are "almost equivalent". Adversarial heuristics generalize ideas from single-agent search algorithms like A* to two-player games, leading to guaranteed lower and upper bounds for the score of a game position. Combining these techniques with state-of-the-art tree search algorithms, our program determines the game-theoretical value of a typical Skat hand (with perfect information) in 10 milliseconds.
Sebastian Kupferschmid, Jörg Hoffmann, Henning Dierks and Gerd Behrmann.
Adapting an AI Planning Heuristic for Directed Model Checking.
In Antti Valmari (ed.), Proceedings of the 13th International SPIN Workshop on Model Checking Software (SPIN 2006), pp. 35-52. Springer-Verlag 2006.
(Show abstract) (Hide abstract) (PDF) (BIB)

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.

2005

Jörg Hoffmann and Sebastian Kupferschmid.
A Covering Problem for Hypercubes.
In Leslie Pack Kaelbling and Alessandro Saffiotti (eds.), Poster Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI 2005), pp. 1523-1524. 2005.
(Show abstract) (Hide abstract) (PDF) (PS.GZ) (BIB)

We introduce a new NP-complete problem asking if a "query" hypercube is (not) covered by a set of other "evidence" hypercubes. This comes down to a form of constraint reasoning asking for the satisfiability of a CNF formula where the logical atoms are inequalities over single variables, with possibly infinite variable domains. We empirically investigate the location of the phase transition regions in two random distributions of problem instances. We introduce a solution method that iteratively constructs a representation of the non-covered part of the query cube. In particular, the method is not based on backtracking. Our experiments show that the method is, in a significant range of instances, superior to the backtracking method that results from translation to SAT, and application of a state-of-the-art DP-based SAT solver.

2003

Sebastian Kupferschmid.
Entwicklung eines Double-Dummy Skat Solvers mit einer Anwendung für verdeckte Skatspiele.
Diploma thesis, Albert-Ludwigs-Universität, Freiburg, Germany 2003.
(Show abstract) (Hide abstract) (PDF) (PS.GZ) (BIB)

In dieser Diplomarbeit werden Monte Carlo Simulation und Alpha-Beta-Suche auf das Skatspiel angewendet. Das entwickelte Skatprogramm integriert bekannte Techniken wie z. B. Zuganordnung (move ordering) mit zwei neuen Sucherweiterungen. Quasi-Symmetrie-Reduktion ist eine Generalisierung von M. Ginsbergs Partition Search, die es erlaubt ähnliche Zustände als symmetrisch anzusehen. Desweiteren wird eine Technik zur schnellen Vorwärtssuche vorgestellt, die Ideen aus dem Gebiet der heuristischen Suche in den Kontext von Zweipersonenspielen transferiert. Die Kombination dieser Techniken zusammen mit einem modernen Algorithmus zur Baumsuche ermöglicht es den spieltheoretischen Wert einer typischen Skathand (mit vollständigem Weltwissen) in 10 Millisekunden zu berechnen.