Rechnerarchitektur - Universität Freiburg

Projekte

CEBug

Projektbeschreibung

Um Fehler in Systemen beheben zu können, ist es essentiell, Gegenbeispiele zur Hand zu haben. Gegenbeispiele sind dabei Systemabläufe die zu einem fehlerhaften Verhalten des Systems führen. Die bisherige Forschung zu stochastischen Systemen konzentrierte sich auf die Berechnung von Wahrscheinlichkeiten, mit denen die Abläufe eines stochastischen Systems eine vorgegebene Eigenschaft erfüllen. Wenn diese Wahrscheinlichkeiten nicht innerhalb der zulässigen Schranken liegen, liefern die verfügbaren Algorithmen zur Modellprüfung zwar die genauen Wahrscheinlichkeitswerte, jedoch keine Gegenbeispiele. Die ersten Schritte zur Berechnung von Gegenbespielen betrachten Markov-Ketten mit diskreter Zeit, eine relativ einfache Klasse von stochastischen Systemen. Das Ziel dieses Projekts ist, auf der einen Seite die verfügbaren Techniken zur Berechnung von Gegenbeispielen zu verbessern und auf der anderen Seite Verfahren zu entwickeln un dzu implementieren, die mit ausdrucksstärkeren Eigenschaften und reichhaltigeren Systemen zurecht kommen. Die praktische Anwendbarkeit unserer Algorithmen werden wir anhand einer Menge von Benchmarks nachweisen. Dieses Projekt wird durch die Deutsche Forschungsgemeinschaft (DFG) gefördert.

Laufzeit

Von 01.01.2011 (unbegrenzt)

Projektleitung

Becker B

Ansprechpartner/in

Wimmer R

WWW: https://ira.informatik.uni-freiburg.de/src/projects_view.php?projectID=57

Publikationen

Jahre: 2015 | 2014 | 2013 | 2012 | 2011

2015

nach oben zur Jahresübersicht

Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
Counterexamples for Expected Rewards
2015 Proceedings of the 20th International Symposium on Formal Methods (FM), Springer, Band: 9109, Seiten: 435 - 452
KurzfassungThe computation of counterexamples for probabilistic systems has gained a lot of attention during the last few years. All of the proposed methods focus on the situation when the probabilities of certain events are too high. In this paper we investigate how counterexamples for properties concerning expected costs (or, equivalently, expected rewards) of events can be computed. We propose methods to extract a minimal subsystem which already leads to costs beyond the allowed bound. Besides these exact methods, we present heuristic approaches based on path search and on best-first search, which are applicable to very large systems when deriving a minimum subsystem becomes infeasible due to the system size. Experiments show that we can compute counterexamples for systems with millions of states.
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
High-level Counterexamples for Probabilistic Automata
2015 Log Meth Comput Sci (Logical Methods In Computer Science), Band: 11, Nummer: 1:15, Seiten: 1 - 23
KurzfassungProviding compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker PRISM. In this paper we describe how a smallest possible subset of the commands can be identified which together make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.

2014

nach oben zur Jahresübersicht

Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer
Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
In: International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), Advanced Lectures
2014, Springer-Verlag, Seiten: 65 - 121,
KurzfassungThis paper is an introductory survey of available methods for the computation and representation of probabilistic counterexamples for discrete-time Markov chains and probabilistic automata. In contrast to traditional model checking, probabilistic counterexamples are sets of finite paths with a critical probability mass. Such counterexamples are not obtained as a by-product of model checking, but by dedicated algorithms. We define what probabilistic counterexamples are and present approaches how they can be generated. We discuss methods based on path enumeration, the computation of critical subsystems, and the generation of critical command sets, both, using explicit and symbolic techniques.
Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
Fast Debugging of PRISM Models
2014 Int'l Symp. on Automated Technology for Verfication and Analysis, Springer-Verlag
KurzfassungIn addition to rigorously checking whether a system conforms to a specification, model checking can provide valuable feedback in the form of succinct and understandable counterexamples. In the context of probabilistic systems, path- and subsystem-based counterexamples at the state-space level can be of limited use in debugging. As many probabilistic systems are described in a guarded command language like the one used by the popular model checker Prism, a technique identifying a subset of critical commands has recently been proposed. Based on repeatedly solving MAXSAT~instances, our novel approach to computing a minimal critical command set achieves a speed-up of up to five orders of magnitude over the previously existing technique.
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Minimal Counterexamples for Linear-Time Probabilistic Verification
2014 Theor Comput Sci
KurzfassungCounterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counterexample-guided abstraction refinement. In this paper, we propose the usage of minimal critical subsystems of discrete-time Markov chains and Markov decision processes as counterexamples for violated omega-regular properties. Minimality can thereby be defined in terms of the number of states or transitions. This problem is known to be NP-complete for Markov decision processes. We show how to compute such subsystems using mixed integer linear programming and evaluate the practical applicability in a number of experiments. They show that our method yields substantially smaller counterexample than using existing techniques.
Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster
Symbolic Counterexample Generation for Large Discrete-Time Markov Chains
2014 Sci Comput Program, Band: 91, Nummer: A, Seiten: 90 - 114
KurzfassungThis paper presents several symbolic counterexample generation algorithms for discrete-time Markov chains (DTMCs) violating a PCTL formula. A counterexample is (a symbolic representation of) a sub-DTMC that is incrementally generated. The crux to this incremental approach is the symbolic generation of paths that belong to the counterexample. We consider two approaches. First, we extend bounded model checking and develop a simple heuristic to generate highly probable paths first. We then complement the SAT-based approach by a fully (multi-terminal) BDD-based technique. All symbolic approaches are implemented, and our experimental results show a substantially better scalability than existing explicit techniques. In particular, our BDD-based approach using a method called fragment search allows for counterexample generation for DTMCs with billions of states (up to 10^{15}).

2013

nach oben zur Jahresübersicht

Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
High-Level Counterexamples for Probabilistic Automata
2013 Springer-Verlag, Band: 8054, Seiten: 18 - 33
KurzfassungProviding compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker \texttt{PRISM}. In this paper we describe how a minimal subset of the commands can be identified which together already make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
High-Level Counterexamples for Probabilistic Automata
, Band: arxiv:1305.5055, 2013
Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám
Stochastic Bounded Model Checking: Bounded Rewards and Compositionality
2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 243 - 254
KurzfassungWe extend the available SAT/SMT-based methods for generating counterexamples of probabilistic systems in two ways: First, we propose bounded rewards, which are appropriate, e. g., to model the energy consumption of autonomous embedded systems, and show how to extend the SMT-based counterexample generation to handle such models. Second, we describe a compositional SAT encoding of the transition relation of Markov models, which exploits the system structure to obtain a more compact formula, which in turn can be solved more efficiently. Preliminary experiments show promising results in both cases.

2012

nach oben zur Jahresübersicht

Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
AVACS Technical Report, Nummer: 88, 2012
Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties
2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Verlag Dr. Kovac, Seiten: 169 - 180
Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
Minimal Critical Subsystems for Discrete-Time Markov Models
2012 Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer-Verlag, Band: 7214, Seiten: 299 - 314
KurzfassungWe propose a new approach to compute counterexamples for violated ω-regular properties of discrete-time Markov chains and Markov decision processes. Whereas most approaches compute a set of system paths as a counterexample, we determine a critical subsystem that already violates the given property. In earlier work we introduced methods to compute such subsystems based on a search for shortest paths. In this paper we use SMT solvers and mixed integer linear programming to determine minimal critical subsystems.
Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker
Symbolic Counterexample Generation for Discrete-time Markov Chains
2012 Int'l Symp. on Formal Aspects of Component Software, Springer-Verlag, Band: 7684, Seiten: 134 - 151
KurzfassungIn this paper we investigate the generation of counterexamples for discrete-time Markov chains (DTMCs) and PCTL properties. Whereas most available methods use explicit representations for at least some intermediate results, our aim is to develop fully symbolic algorithms. As in most related work, our counterexample computations are based on path search. We first adapt bounded model checking as a path search algorithm and extend it with a novel SAT-solvingheuristics to prefer paths with higher probabilities. As a second approach, we use symbolic graph algorithms to find counterexamples. Experiments show that our approaches, in contrast to other existing techniques, are applicable to very large systems with millions of states.
Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
The COMICS Tool - Computing Minimal Counterexamples for DTMCs
2012 Automated Technology for Verification and Analysis, Springer-Verlag, Band: 7561, Seiten: 349 - 353
KurzfassungThis paper presents the tool COMICS 1.0, which performs model checking and generates counterexamples for DTMCs. For an input DTMC, COMICS computes an abstract system that carries the model checking information and uses this result to compute a critical subsystem, which induces a counterexample. This abstract subsystem can be refined and concretized hierarchically. The tool comes with a command line version as well as a graphical user interface that allows the user to interactively influence the refinement process of the counterexample.
Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
The COMICS Tool - Computing Minimal Counterexamples for DTMCs
, Band: arxiv:1206.0603, 2012

2011

nach oben zur Jahresübersicht

Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking
2011 IFIP Int'l Conf. on Formal Methods for Open Object-based Distributed Systems, Springer-Verlag, Band: 6722, Seiten: 75 - 89
KurzfassungGeneration of counterexamples is a highly important task in the model checking process. In contrast to, e.\,g., digital circuits where counterexamples typically consist of a single path leading to a critical state of the system, in the probabilistic setting counterexamples may consist of a large number of paths. In order to be able to handle large systems and to use the capabilities of modern SAT-solvers, bounded model checking (BMC) for discrete-time Markov chains was established.\par In this paper we introduce the usage of SMT-solving over linear real arithmetic for the BMC procedure. SMT-solving, extending SAT with theories in this context on the one hand leads to a convenient way to express conditions on the probability of certain paths and on the other hand allows to handle Markov reward models. We use the former to find paths with high probability first. This leads to more compact counterexamples. We report on some experiments, which show promising results.
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Hierarchical Counterexamples for Discrete-Time Markov Chains
2011 Int'l Symp. on Automated Technology for Verification and Analysis, Springer-Verlag, Band: 6996, Seiten: 443 - 452
KurzfassungThis paper introduces a novel counterexample generation approach for the verification of discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate abstract counterexamples which can be refined in a hierarchical manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a critical subsystem of the DTMC whose paths form a counterexample. Experiments show that with our approach we can reduce the size of counterexamples and the number of computation steps by several orders of magnitude.
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Hierarchical Counterexamples for Discrete-Time Markov Chains
, Band: AIB-2011-11, 2011
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
SMT-based Counterexample Generation for Markov Chains
2011 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Offis Oldenburg, Band: 14, Seiten: 19 - 28
KurzfassungCounterexamples are a highly important feature of the model checking process. In contrast to, e.\,g., digital circuits where counterexamples typically consist of a single path leading to a critical state of the system, in the probabilistic setting, counterexamples may consist of a large number of paths. In order to be able to handle large systems and to use the capabilities of modern SAT-solvers, bounded model checking (BMC) for discrete-time Markov chains was established.In this paper we introduce the usage of SMT-solving over the reals for the BMC procedure. SMT-solving, extending SAT with theories, leads in this context on the one hand to a convenient way to express conditions on the probability of certain paths and on the other hand to handle Markov Reward models. The former can be used to find paths with high probability first. This leads to more compact counterexamples.We report on some experiments, which show promising results.