apl. Prof. Dr. Ralf Wimmer

Publications

A publication list for download can be found here.

2021

• Pascal Pieper, Ralf Wimmer, Gerhard Angst, Rolf Drechsler: Minimally Invasive HW/SW Co-debug Live Visualization on Architecture Level
  Proceedings of the 31^st ACM Great Lakes Symposium on VLSI (GLSVLSI), ACM Press, 2021
  pdf-file, BibTeX
  ► Abstract
  We present a tool that allows developers to debug hard- and software and their interaction in an early design stage. We combine a SystemC virtual prototype (VP) with an easily configurable and interactive graphical user interface and a standard software debugger. The graphical user interface visualizes the internal state of the hardware. At the same time, the software debugger monitors and allows to manipulate the state of the software. This co-visualization supports design understanding and live debugging of the HW/SW interaction. We demonstrate its usefulness with a case-study where we debug an OLED display driver running on a RISC-V VP.
• Leonore Winterer, Ralf Wimmer, Nils Jansen, Bernd Becker: Strengthening Deterministic Strategies for POMDPs (Extended Abstract)
  Informal Proceedings of the 24^th GI/ITG/GMM Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), 2021
  pdf-file, BibTeX
  ► Abstract
  Computing strategies for partially observable Markov decision processes that ensure a certain desired behavior is an undecidable problem. Such optimal strategies typically require the knowledge of the full history, i. e., infinite memory. Instead, we propose solver-based algorithms for stationary algorithms that only depend on the current state instead of the whole history. Since computing optimal stationary, but randomized strategies is still too costly, we resort to determinstic stationary strategies and algorithms using mixed-integer programming. We show how to allow a certain amount of randomization and how to incorporate some knowledge of the history by applying state- and observation splitting. Our experiments demonstrate that these methods are competitive to traditional POMDP algorithms.
• Aile Ge-Ernst, Christoph Scholl, Juraj S\'\i\vc, Ralf Wimmer: Solving Dependency Quantified Boolean Formulas Using Quantifier Localization
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications which can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, research focused on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), while non-prenex DQBFs have almost not been studied in the literature. In this paper, we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the-art DQBF solver. Experiments with prenex DQBF benchmarks, including all instances from the QBFEVAL'18–'20 competitions, clearly show that quantifier localization pays off in this context.
• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker: Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions
  IEEE Transactions on Automatic Control, 66(3), pages 1040–1054, 2021
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We study synthesis problems with constraints in partially observable Markov decision processes (POMDPs), where the objective is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Verification and strategy synthesis for POMDPs are, however, computationally intractable in general. We alleviate this difficulty by focusing on planning applications and exploiting typical structural properties of such scenarios; for instance, we assume that the agent has the ability to observe its own position inside an environment. We propose an abstraction refinement framework which turns such a POMDP model into a (fully observable) probabilistic two-player game (PG). For the obtained PGs, efficient verification and synthesis tools allow to determine strategies with optimal safety and performance measures, which approximate optimal schedulers on the POMDP. If the approximation is too coarse to satisfy the given specifications, an refinement scheme improves the computed strategies. As a running example, we use planning problems where an agent moves inside an environment with randomly moving obstacles and restricted observability. We demonstrate that the proposed method advances the state of the art by solving problems several orders-of-magnitude larger than those that can be handled by existing POMDP solvers. Furthermore, this method gives guarantees on safety constraints, which is not supported by the majority of the existing solvers.

2020

• Leonore Winterer, Ralf Wimmer, Nils Jansen, Bernd Becker: Strengthening Deterministic Policies for POMDPs
  Proceedings of the 12^th NASA Formal Methods Symposium (NFM), Lecture Notes in Computer Science, vol. 12229, pages 115–132, Springer, 2020
  pdf-file, BibTeX , Original Publication
  ► Abstract
  The synthesis problem for partially observable Markov decision processes (POMDPs) is to compute a policy that satisfies a given specification. Such policies have to take the full execution history of a POMDP into account, rendering the problem undecidable in general. A common approach is to use a limited amount of memory and randomize over potential choices. Yet, this problem is still NP-hard and often computationally intractable in practice. A restricted problem is to use neither history nor randomization, yielding policies that are called stationary and deterministic. Previous approaches to compute such policies employ mixed-integer linear programming (MILP). We provide a novel MILP encoding that supports sophisticated specifications in the form of temporal logic constraints. It is able to handle an arbitrary number of such specifications. Yet, randomization and memory are often mandatory to achieve satisfactory policies. First, we extend our encoding to deliver a restricted class of randomized policies. Second, based on the results of the original MILP, we employ a preprocessing of the POMDP to encompass memory-based decisions. The advantages of our approach over state-of-the-art POMDP solvers lie (1)~in the flexibility to strengthen simple deterministic policies without losing computational tractability and (2)~in the ability to enforce the provable satisfaction of arbitrarily many specifications. The latter point allows to take trade-offs between performance and safety aspects of typical POMDP examples into account. We show the effectiveness of our method on a broad range of benchmarks.

2019

• Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst: A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving
  Proceedings of the 33^rd AAAI Conference on Artificial Intelligence (AAAI), pages 1584–1591, AAAI Press, 2019
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. This enables a succinct encoding of decision problems in the NEXPTIME complexity class. As solving general DQBFs is NEXPTIME complete, in contrast to the PSPACE completeness of QBF solving, characterizing DQBF subclasses of lower computational complexity allows their effective solving and is of practical importance.
  Recently a DQBF proof calculus based on a notion of fork extension, in addition to resolution and universal reduction, was proposed by Rabe in 2017. We show that this calculus is in fact incomplete for general DQBFs, but complete for a subclass of DQBFs, where any two existential variables have either identical or disjoint dependency sets over the universal variables. We further characterize this DQBF subclass to be $\Sigma_3^\mathrmP$ complete in the polynomial time hierarchy. Essentially using fork extension, a DQBF in this subclass can be converted to an equisatisfiable 3QBF with only a linear increase in formula size. We exploit this conversion for effective solving of this DQBF subclass and point out its potential as a general strategy for DQBF quantifier localization. Experimental results show that the method outperforms state-of-the-art DQBF solvers on a number of benchmarks, including the 2018 DQBF evaluation benchmarks.
• Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer: Localizing Quantifiers for DQBF
  Proceedings of the 19^th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 184–192, IEEE, 2019
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications that can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, most works focus on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula), and non-prenex DQBFs have almost not been studied in the literature. In this paper we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the-art DQBF solver. Experiments with prenex DQBF benchmarks, including those from the QBFEVAL'18 competition, clearly show that quantifier localization pays off in this context.
• Steven Carr, Nils Jansen, Ralf Wimmer and Alexandru Constantin Serban, Bernd Becker, Ufuk Topcu: Counterexample-Guided Strategy Improvement for POMDPs using Recurrent Neural Networks
  Proceedings of the 28^th International Joint Conference on Artificial Intelligence (IJCAI), pages 5532–5539, ijcai.org, 2019
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We study strategy synthesis for POMDPs. The particular problem is to determine strategies that provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable and theoretically hard. We propose a novel method that combines techniques from machine learning and formal verification. First, we train an RNN to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy to represent a finite-memory strategy and implement it on a specific POMDP. For the resulting finite Markov chain, efficient formal verification techniques provide provable guarantees against temporal logic specifications. If the specification is not satisfied, counterexamples supply diagnostic information. We use this information to improve the strategy by iteratively training the RNN. Numerical experiments show that the proposed method elevates the state of the art in POMDP solving by up to three orders of magnitude in terms of solving times and model sizes.
• Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer: Quantifier Localization for DQBF
  Informal Proceedings of the 28^th International Workshop on Logic & Synthesis (IWLS), 2019
  pdf-file, BibTeX
  ► Abstract
  Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications which can be encoded by DQBFs in a natural, compact and elegant way, research on DQBF solving has emerged in the past few years. However, research focused on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula); non-prenex DQBFs have almost not been studied, apart from one seminal work \citeBalabanovCJ14, which considers –~as a side remark~– quantifier localization for DQBF, transforming prenex DQBFs into non-prenex DQBFs. However, in that work the semantics of non-prenex DQBFs is not formally defined and, in addition, the two propositions allowing quantifier localization are not sound, as we will show in our paper. We close this gap by providing a definition for syntax and semantics of non-closed non-prenex DQBFs and by formally proving useful properties. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the-art DQBF solver. Experiments with prenex DQBF benchmarks from the QBFEVAL'18 competition clearly show that quantifier localization pays off in this context.
• Ralf Wimmer, Christoph Scholl, Bernd Becker: The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation
  Journal on Satisfiability, Boolean Modeling and Computation, 11(1), pages 3–52, 2019
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Preprocessing turned out to be an essential step for SAT, QBF, and DQBF solvers to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. These preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper, we present the preprocessor HQSpre that was developed for Dependency Quantified Boolean Formulas (DQBFs) and generalizes different preprocessing techniques for SAT and QBF problems to DQBF. We give a presentation of the underlying theory together with detailed proofs as well as implementation details contributing to the efficiency of the preprocessor. HQSpre has been used with obvious success by the winners of the DQBF track, and, even more interestingly, the QBF tracks of QBFEVAL'18.
• Nils Jansen, Steven Carr, Alexandru Constantin Serban, Ralf Wimmer and Ufuk Topcu, Bernd Becker: Coun\-ter\-example-Guided Strategy Improvement for POMDPs using Recurrent Neural Networks
  Proceedings of the 3^rd Workshop on Learning in Verification (LiVe), 2019
  pdf-file, BibTeX
• Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer: Localizing Quantifiers for DQBF
  Proceedings of the International Workshop on Quantified Boolean Formulas and Beyond (QBF), 2019
  pdf-file, BibTeX
  ► Abstract
  Dependency quantified Boolean formulas (DQBFs) are a powerful formalism which allows a variety of applications to be encoded in a natural and elegant way. So far, research has focused on closed DQBFs in prenex form, and non-prenex DQBFs have almost not been studied in the literature. In our work, we provide a formal definition for the syntax and semantics of non-closed non-prenex DQBFs and prove useful properties to enable quantifier localization. We show the effectiveness of applying our approach on prenex DQBF benchmarks including those from the QBFEVAL'18 competition.
• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen and Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker: Strategy Synthesis in POMDPs via Game-Based Abstractions
  Proceedings of the RSS-Workshop on Safe Autonomy (RSS-Safe), 2019
  pdf-file, BibTeX
  ► Abstract
  Partially observable Markov decision processes (POMDPs) are a natural model for scenarios where one has to deal with incomplete knowledge and random events. Applications include, but are not limited to, robotics and motion planning. However, many relevant properties of POMDPs are either undecidable or very expensive to compute in terms of both runtime and memory consumption. In our work, we develop a game-based abstraction method that is able to deliver safe bounds and tight approximations for important sub-classes of such properties. We discuss the theoretical implications and showcase the applicability of our results on a broad spectrum of benchmarks.
• Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer: Correct-by-Construction Policies for POMDPs
  Proceedings of the 5^th International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR), pages 6–8, ACM Press, 2019
  pdf-file, BibTeX , Original Publication
  ► Abstract
  In this extended abstract, we discuss how to compute policies with finite memory–-so-called finite-state controllers (FSCs)–-for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. In particular, for a POMDP $M$ and a specification $\varphi$, we want to solve the decision problem whether there is a policy $\sigma$ for $M$ with $k$ memory states, such that $\varphi$ is satisfied by $M$ and $\sigma$ ($M^\sigma\models\varphi$). The underlying method is achieved via a marriage of formal verification and artificial intelligence. The key insight is that computing (randomized) FSCs on POMDPs is equivalent to–-and computationally as hard as–-synthesis for parametric Markov chains (pMCs). The parameter synthesis problem is to decide whether for a parametric Markov chain (pMC) $D$ and a specification $\varphi$ there is a parameter instantiation $u$ such that in the Markov chain (MC) induced by $u$ the specification is satisfied ($M[u]\models\varphi$). The correspondence allows to utilize efficient tools for synthesis in pMCs to compute correct-by-construction FSCs on POMDPs.
• Steven Carr, Nils Jansen, Ralf Wimmer and Alexandru Constantin Serban, Bernd Becker, Ufuk Topcu: Coun\-ter\-example-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  We study strategy synthesis for POMDPs. The particular problem is to determine strategies that provably adhere to (probabilistic) temporal logic constraints. This problem is computationally intractable and theoretically hard. We propose a novel method that combines techniques from machine learning and formal verification. First, we train a RNN to encode POMDP strategies. The RNN accounts for memory-based decisions without the need to expand the full belief space of a POMDP. Secondly, we restrict the RNN-based strategy to represent a finite-memory strategy and implement it on a specific POMDP. For the resulting finite Markov chain, efficient formal verification techniques provide provable guarantees against temporal logic specifications. If the specification is not satisfied, counterexamples supply diagnostic information. We use this information to improve the strategy by iteratively training the RNN. Numerical experiments show that the proposed method elevates the state of the art in POMDP solving by up to three orders of magnitude in terms of solving times and model sizes.

2018

• Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker: Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
  Advanced Logic Synthesis, pages 151–168, Springer, 2018
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural calculus to exactly express the realizability problem of incomplete combinational and sequential circuits with an arbitrary number of (combinational or bounded-memory) black boxes. In contrast to usual approaches for controller synthesis, restrictions to the interfaces of missing circuit parts in distributed architectures are strictly taken into account. We present a solution method for DQBFs together with the extraction of Skolem functions for existential variables, which can directly serve as implementations for the black boxes. First experimental results are provided.
• Bernd Becker, Christoph Scholl, Ralf Wimmer: Verification of Incomplete Designs
  Formal System Verification – State of the Art and Future Trends, pages 37–72, Springer, 2018
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We consider the verification of digital systems which are incomplete in the sense that for some modules only their interfaces (i.e., the signals entering and leaving the module) are known, but not their implementations. For such designs, we study realizability („Is it possible to implement the missing modules such that the complete design has certain properties?”) and validity („Does a property hold no matter how the missing parts are implemented?”).
• Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu, Ufuk Topcu: Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes
  Proceedings of the 2018 Annual American Control Conference (ACC), pages 762–769, IEEE, 2018
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We study planning problems where autonomous agents operate inside environments that are subject to uncertainties and not fully observable. Partially observable Markov decision processes (POMDPs) are a natural formal model to capture such problems. Because of the potentially huge or even infinite belief space in POMDPs, synthesis with safety guarantees is, in general, computationally intractable. We propose an approach that aims to circumvent this difficulty: in scenarios that can be partially or fully simulated in a virtual environment, we actively integrate a human user to control an agent. While the user repeatedly tries to safely guide the agent in the simulation, we collect data from the human input. Via behavior cloning, we translate the data into a strategy for the POMDP. The strategy resolves all nondeterminism and non-observability of the POMDP, resulting in a discrete-time Markov chain (MC). The efficient verification of this MC gives quantitative insights into the quality of the inferred human strategy by proving or disproving given system specifications. For the case that the quality of the strategy is not sufficient, we propose a refinement method using counterexamples presented to the human. Experiments show that by including humans into the POMDP verification loop we improve the state of the art by orders of magnitude in terms of scalability.
• Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker: From DQBF to QBF by Dependency Elimination (Extended Abstract)
  Proceedings of the 21^st GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2018
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Dependency quantified Boolean formulas (DQBFs) are a generalization of QBFs, which allows to have existential variables that depend on arbitrary subsets of the universal variables. We present an effective way to solve such DQBFs by eliminating individual dependencies such that an equisatisfiable QBF is obtained, which can be solved by an arbitrary QBF solver. We also present how to use dependency schemes in order to obtain smaller equisatisfiable QBFs, which can typically be solved more efficiently.
• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker: Abstraktions-basierte Verifikation von POMDPs im Motion-Planning Kontext (Extended Abstract)
  Proceedings of the 21^st GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, 2018
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Wir untersuchen Pfadplanungsprobleme aus der Robotik und die Berechnung von Strategien, die beweisbare Garantien für Sicherheitseigenschaften liefern. Dabei soll ein Agent mit hoher Wahrscheinlichkeit einen Zielort erreichen, ohne mit einem Hindernis zusammenzustoßen, das sich probabilistisch durch den Raum bewegt. Schwierig wird dieses Problem dadurch, dass der Agent seine Umgebung nur eingeschränkt beobachten kann. Dieses Szenario lässt sich auf natürliche Art und Weise als ein sogenannter partiell beobachtbarer Markow-Entscheidungsprozess (POMDP) modellieren. Da viele interessante Eigenschaften auf POMDPs unentscheidbar sind, beschäftigt sich die hier vorgestellte Arbeit mit der Entwicklung einer spielbasierten Abstraktionsmethode, um für solche Pfadplanungsprobleme und Sicherheitseigenschaften gute Approximationen zu berechnen.
• Yuliya Butkova, Ralf Wimmer, Holger Hermanns: Markov Automata on Discount!
  Proceedings of the 19^th International GI/ITG Conference on Measurement, Modelling and Evaluation of Computing Systems (MMB), Lecture Notes in Computer Science, vol. 10740, pages 19–34, Springer, 2018
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Markov automata (MA) are a rich modelling formalism for complex systems combining compositionality with probabilistic choices and continuous stochastic timing. Model checking algorithms for different classes of properties involving probabilities and rewards have been devised for MA, opening up a spectrum of applications in dependability engineering and artificial intelligence, reaching out into economy and finance. In the latter more general contexts, several quantities of considerable importance are based on the idea of discounting reward expectations, so that the near future is more important than the far future. This paper introduces the expected discounted reward value for MA and develops effective iterative algorithms to quantify it, based on value- as well as policy-iteration. To arrive there, we reduce the problem to the computation of expected discounted rewards and expected total rewards in Markov decision processes. This allows us to adapt well-known algorithms to the MA setting. Experimental results clearly show that our algorithms are efficient and scale to MA with hundred thousands of states.
• Christoph Scholl, Ralf Wimmer: Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
  Proceedings of the 21^st International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 10929, pages 3–16, Springer, 2018
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Dependency quantified Boolean formulas (DQBFs) as a generalization of quantified Boolean formulas (QBFs) have received considerable attention in research during the last years. Here we give an overview of the solution methods developed for DQBF so far. The exposition is complemented with the discussion of various applications that can be handled with DQBF solving.
• Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu, Ufuk Topcu: Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  We study planning problems where autonomous agents operate inside environments that are subject to uncertainties and not fully observable. Partially observable Markov decision processes (POMDPs) are a natural formal model to capture such problems. Because of the potentially huge or even infinite belief space in POMDPs, synthesis with safety guarantees is, in general, computationally intractable. We propose an approach that aims to circumvent this difficulty: in scenarios that can be partially or fully simulated in a virtual environment, we actively integrate a human user to control an agent. While the user repeatedly tries to safely guide the agent in the simulation, we collect data from the human input. Via behavior cloning, we translate the data into a strategy for the POMDP. The strategy resolves all nondeterminism and non-observability of the POMDP, resulting in a discrete-time Markov chain (MC). The efficient verification of this MC gives quantitative insights into the quality of the inferred human strategy by proving or disproving given system specifications. For the case that the quality of the strategy is not sufficient, we propose a refinement method using counterexamples presented to the human. Experiments show that by including humans into the POMDP verification loop we improve the state of the art by orders of magnitude in terms of scalability.
• Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker: Finite-State Controllers of POMDPs via Parameter Synthesis
  Proceedings of the 34^th Conference on Uncertainty in Artificial Intelligence (UAI), pages 519–529, AUAI Press, 2018
  pdf-file, BibTeX
  ► Abstract
  We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to (and computationally as hard as) synthesis for parametric Markov chains (pMCs). This correspondence enables using black-box techniques to compute correct-by-construction FSCs for POMDPs for a wide range of properties. Our experimental evaluation on typical POMDP problems shows that we are competitive to state-of-the-art POMDP solvers.

2017

• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker: Motion Planning under Partial Observability using Game-Based Abstraction
  Proceedings of the 56^th IEEE Conference on Decision and Control (CDC), pages 2201–2208, IEEE, 2017
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We study motion planning problems where agents move inside environments that are not fully observable and subject to uncertainties. The goal is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Such problems are naturally modeled by partially observable Markov decision processes (POMDPs). Because of the potentially huge or even infinite belief space of POMDPs, verification and strategy synthesis is in general computationally intractable. We tackle this difficulty by exploiting typical structural properties of such scenarios; for instance, we assume that agents have the ability to observe their own positions inside an environment. Ambiguity in the state of the environment is abstracted into non-deterministic choices over the possible states of the environment. Technically, this abstraction transforms POMDPs into probabilistic two-player games (PGs). For these PGs, efficient verification tools are able to determine strategies that approximate certain measures on the POMDP. If an approximation is too coarse to provide guarantees, an abstraction refinement scheme further resolves the belief space of the POMDP. We demonstrate that our method improves the state of the art by orders of magnitude compared to a direct solution of the POMDP.
• Hassan Hatefi, Ralf Wimmer, Bettina Braitling and Luis María Ferrer Fioriti, Bernd Becker, Holger Hermanns: Cost vs. Time in Stochastic Games and Markov Automata
  Formal Aspects of Computing, 29(4), pages 629–649, 2017
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and Markov games. We provide a fixed point characterization of this class of properties under early schedulers. Additionally, we give a transformation to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of Markov automata case studies.
• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker: Abstraction-based Model Checking of POMDPs in Motion Planning
  Proceedings of the PhD Symposium at iFM'17 on Formal Methods: Algorithms, Tools and Applications (PhD-iFM), 2017
  pdf-file, BibTeX
  ► Abstract
  Partially observable Markov decision processes (POMDPs) are a natural model for many applications where one has to deal with incomplete knowledge and random phenomena, including, but not limited to, robotics and motion planning. However, many interesting properties of POMDPs are undecidable or otherwise very expensive to decide in terms of both runtime and memory usage. In our work, we develop abstraction-based methods that can deliver safe bounds and good approximations for certain classes of properties.
• Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker: From DQBF to QBF by Dependency Elimination
  Proceedings of the 20^th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 10491, pages 326–343, Springer, 2017
  pdf-file, BibTeX , Original Publication
  ► Abstract
  In this paper, we propose the elimination of dependencies to convert a given dependency quantified Boolean formula (DQBF) to an equisatisfiable QBF. We show how to select a set of dependencies to eliminate such that we arrive at a smallest equisatisfiable QBF in terms of existential variables that is achievable using dependency elimination. This approach is improved by taking so-called don't-care dependencies into account, which result from the application of dependency schemes to the formula and can be added to or removed from the formula at no cost. We have implemented this new method in the state-of-the-art DQBF solver HQS. Experiments show that dependency elimination is clearly superior to the previous method using variable elimination.
• Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd Becker: HQSpre – An Effective Preprocessor for QBF and DQBF
  Proceedings of the 23^rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part~I, Lecture Notes in Computer Science, vol. 10205, pages 373–390, Springer, 2017
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We present our new preprocessor HQSpre, a state-of-the-art tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting from adding so-called Henkin-quantifiers to QBFs. HQSpre applies most of the preprocessing techniques that have been proposed in the literature. It can be used both as a standalone tool and as a library. It is possible to tailor it towards different solver back-ends, e. g., to preserve the circuit structure of the formula when a non-CNF solver back-end is used. Extensive experiments show that HQSpre allows QBF solvers to solve more benchmark instances and is able to decide more instances on its own than state-of-the-art tools. The same impact can be observed in the DQBF domain as well.
• Yuliya Butkova, Ralf Wimmer, Holger Hermanns: Long-run Rewards for Markov Automata
  Proceedings of the 23^rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part~II, Lecture Notes in Computer Science, vol. 10206, pages 188–203, Springer, 2017
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Markov automata are a powerful formalism for modelling systems which exhibit nondeterminism, probabilistic choices and continuous stochastic timing. We consider the computation of long-run average rewards, the most classical problem in continuous-time Markov model analysis. We propose an algorithm based on value iteration. It improves the state of the art by orders of magnitude. The contribution is rooted in a fresh look on Markov automata, namely by treating them as an efficient encoding of CTMDPs with –~in the worst case~– exponentially more transitions.
• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen and Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker: Motion Planning under Partial Observability using Game-Based Abstraction
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  We study motion planning problems where agents move inside environments that are not fully observable and subject to uncertainties. The goal is to compute a strategy for an agent that is guaranteed to satisfy certain safety and performance specifications. Such problems are naturally modelled by partially observable Markov decision processes (POMDPs). Because of the potentially huge or even infinite belief space of POMDPs, verification and strategy synthesis is in general computationally intractable. We tackle this difficulty by exploiting typical structural properties of such scenarios; for instance, we assume that agents have the ability to observe their own positions inside an environment. Ambiguity in the state of the environment is abstracted into non-deterministic choices over the possible states of the environment. Technically, this abstraction transforms POMDPs into probabilistic two-player games (PGs). For these PGs, efficient verification tools are able to determine strategies that approximate certain measures on the POMDP. If an approximation is too coarse to provide guarantees, an abstraction refinement scheme further resolves the belief space of the POMDP. We demonstrate that our method improves the state of the art by orders of magnitude compared to a direct solution of the POMDP.
• Sebastian Junges, Nils Jansen, Ralf Wimmer and Joost-Pieter Katoen, Bernd Becker: Permissive Finite-state Controllers of POMDPs using Parameter Synthesis
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  We study finite-state controllers (FSCs) for partially observable Markov decision processes (POMDPs) that are provably correct with respect to given specifications. The key insight is that computing (randomised) FSCs on POMDPs is equivalent to–-and computationally as hard as–-synthesis for parametric Markov chains (pMCs). This correspondence allows to use tools for parameter synthesis in pMCs to compute correct-by-construction FSCs on POMDPs for a variety of specifications. Our experimental evaluation shows comparable performance to well-known POMDP solvers.

2016

• Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Skolem Functions for DQBF
  Proceedings of the 14^th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 9938, pages 395–411, Springer, 2016
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.
• Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker: Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
  Informal Proceedings of the 25^th International Workshop on Logic & Synthesis (IWLS), pages 50–57, 2016
  pdf-file, BibTeX
  ► Abstract
  We consider Dependency Quantified Boolean Formulas (DQBFs), a generalization of Quantified Boolean Formulas (QBFs), and demonstrate that DQBFs are a natural calculus to exactly express the realizability problem of incomplete combinational and sequential circuits with an arbitrary number of (combinational or bounded-memory) black boxes. In contrast to usual approaches for controller synthesis, restrictions to the interfaces of missing circuit parts in distributed architectures are strictly taken into account. We present a solution method for DQBFs together with the extraction of Skolem functions for existential variables, which can directly serve as implementations for the black boxes. First experimental results are provided.
• Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker: Dependency Schemes for DQBF
  Proceedings of the 19^th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 9710, pages 473–489, Springer, 2016
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Dependency schemes allow to identify variable independencies in QBFs or DQBFs. For QBF, several dependency schemes have been proposed, which differ in the number of independencies they are able to identify. In this paper, we analyze the spectrum of dependency schemes that were proposed for QBF. It turns out that only some of them are sound for DQBF. For the sound ones, we provide a correctness proof, for the others counterexamples. Experiments show that a significant number of dependencies can either be added to or removed from a formula without changing its truth value, but with significantly increasing the flexibility for modifying the representation.
• Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Skolem Functions for DQBF (extended version)
  Technical report.
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We consider the problem of computing Skolem functions for satisfied dependency quantified Boolean formulas (DQBFs). We show how Skolem functions can be obtained from an elimination-based DQBF solver and how to take preprocessing steps into account. The size of the Skolem functions is optimized by don't-care minimization using Craig interpolants and rewriting techniques. Experiments with our DQBF solver HQS show that we are able to effectively compute Skolem functions with very little overhead compared to the mere solution of the formula.

2015

• Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker: Solving DQBF through Quantifier Elimination
  Proceedings of the International Conference on Design, Automation & Test in Europe (DATE), pages 1617–1622, IEEE, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We show how to solve dependency-quantified Boolean formulas (DQBF) using a quantifier elimination strategy which yields an equivalent QBF that can be decided using any standard QBF solver. The elimination is accompanied by a number of optimizations which help reduce memory consumption and computation time.
  We apply our solver HQS to problems from the domain of verification of incomplete combinational circuits to demonstrate the effectiveness of the proposed algorithm. The results show enormous improvements both in the number of solved instances and in the computation times compared to existing work on validating DQBF.
• Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám and Joost-Pieter Katoen, Bernd Becker: Counterexamples for Expected Rewards
  Proceedings of the 20^th International Symposium on Formal Methods (FM), Lecture Notes in Computer Science, vol. 9109, pages 435–452, Springer, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  The 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
  Logical Methods in Computer Science, 11(1:15), pages 1-23, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Providing 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.
• Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd Becker: Towards Verification of Artificial Neural Networks
  Proceedings of the 18^th GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 30–40, Technische Universität Chemnitz, Germany, 2015
  pdf-file, BibTeX
  ► Abstract
  We consider the safety verification of controllers obtained via machine learning. This is an important problem as the employed machine learning techniques work well in practice, but cannot guarantee safety of the produced controller, which is typically represented as an artificial neural network. Nevertheless, such methods are used in safety-critical environments.\
  In this paper we take a typical control problem, namely the Cart Pole System (a.k.a. inverted pendulum), and a model of its physical environment and study safety verification of this system. To do so, we use bounded model checking (BMC). The created formulas are solved with the SMT-solver iSAT3. We examine the problems that occur during solving these formulas and show that extending the solver by special deduction routines can reduce both memory consumption and computation time on such instances significantly. This constitutes a first step towards verification of machine-learned controllers, but a lot of challenges remain.
• Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker: Preprocessing for DQBF
  Proceedings of the 18^th International Conference on Theory and Applications of Satisfiability Testing (SAT), Lecture Notes in Computer Science, vol. 9340, pages 173–190, Springer, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  For SAT and QBF formulas many techniques are applied in order to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. It is well known that these preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper we generalize different preprocessing techniques for SAT and QBF problems to dependency quantified Boolean formulas (DQBF) and describe how they need to be adapted to work with a DQBF solver core. We demonstrate their effectiveness both for CNF- and non-CNF-based DQBF algorithms.
• Hassan Hatefi, Bettina Braitling, Ralf Wimmer, Luis María Ferrer Fioriti, Holger Hermanns, Bernd Becker: Cost vs. Time in Stochastic Games and Markov Automata
  Proceedings of the 1^st International Symposium on Dependable Software Engineering: Theory, Tools and Applications (SETTA), Lecture Notes in Computer Science, vol. 9409, pages 19–34, Springer, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and stochastic games. We give a transformation of this class of properties to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of case studies.
• Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf Wimmer: Modeling Unknown Values in Test and Verification
  Formal Modeling and Verification of Cyber-Physical Systems (Proceedings of the 1^st International Summer School on Methods and Tools for the Design of Digital Systems), pages 122–150, Springer, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  With increasing complexities and a component-based design style the handling of unkown values (e. g., at the interface of components) becomes more and more important in electronic design automation (EDA) and production processes. Tools are required that allow an accurate modeling of unkowns in combination with algorithms balancing exactness of representation and efficiency of calculation. In the following, state-of-the-art approaches are described that enable an efficient and successful handling of unknown values using formal techniques in the areas of Test and Verification.
• Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker: Solving DQBF Through Quantifier Elimination
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  We show how to solve dependency quantified Boolean formulas (DQBF) using a quantifier elimination strategy which yields an equivalent QBF that can be decided using any standard QBF solver. The elimination is accompanied by a number of optimizations which help reduce memory consumption and computation time.
  We apply our solver HQS to problems from the domain of verification of incomplete combinational circuits and demonstrate the effectiveness of the proposed algorithm. The results show enormous improvements both in the number of solved instances and in the computation times compared to existing work on validating DQBF.
• Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker: Preprocessing for DQBF
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  For SAT and QBF formulas many techniques are applied in order to reduce/modify the number of variables and clauses of the formula, before the formula is passed to the actual solving algorithm. It is well known that these preprocessing techniques often reduce the computation time of the solver by orders of magnitude. In this paper we generalize different preprocessing techniques for SAT and QBF problems to dependency quantified Boolean formulas (DQBF) and describe how they need to be adapted to work with a DQBF solver core. We demonstrate their effectiveness both for CNF- and non-CNF-based DQBF algorithms.
• Hassan Hatefi, Bettina Braitling, Ralf Wimmer, Luis María Ferrer Fioriti, Holger Hermanns, Bernd Becker: Cost vs. Time in Stochastic Games and Markov Automata
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and stochastic games. We give a transformation of this class of properties to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of case studies.
• Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd Becker: Transient Reward Approximation for Continuous-Time Markov Chains
  IEEE Transactions on Reliability, 64(4), pages 1254–1275, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We are interested in the analysis of very large continuous-time Markov chains (CTMCs) with many distinct rates. Such models arise naturally in the context of the reliability analysis, e. g., of computer networks performability analysis, of power grids, of computer virus vulnerability, and in the study of crowd dynamics. We use abstraction techniques together with novel algorithms for the computation of bounds on the expected final and accumulated rewards in continuous-time Markov decision processes (CTMDPs). These ingredients are combined in a partly symbolic and partly explicit (symblicit) analysis approach. In particular, we circumvent the use of multi-terminal decision diagrams, because the latter do not work well if facing a large number of different rates. We demonstrate the practical applicability and efficiency of the approach on two case studies.
• Bettina Braitling, Luis María Ferrer Fioriti and Hassan Hatefi, Ralf Wimmer and Holger Hermanns, Bernd Becker: Abstraction-based Computation of Reward Measures for Markov Automata
  Proceedings of the 16^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Lecture Notes in Computer Science, vol. 8931, pages 172–189, Springer, 2015
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Markov automata allow us to model a wide range of complex real-life systems by combining continuous stochastic timing with probabilistic transitions and nondeterministic choices. By adding a reward function it is possible to model costs like the energy consumption of a system as well.
  However, models of real-life systems tend to be large, and the analysis methods for such powerful models like Markov (reward) automata do not scale well, which limits their applicability. To solve this problem we present an abstraction technique for Markov reward automata, based on stochastic games, together with automatic refinement methods for the computation of time-bounded accumulated reward properties. Experiments show a significant speed-up and reduction in system size compared to direct analysis methods.

2014

• Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen: Fast Debugging of PRISM Models
  Proceedings of the 12^th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 8837, pages 146–162, Springer, 2014
  pdf-file, BibTeX , Original Publication
  ► Abstract
  In 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, Erika Ábrahám: Maybe or Maybe Not – Contributions to Stochastic Verification
  Aspekte der Technischen Informatik: Festschrift zum 60. Geburtstag von Bernd Becker, pages 119–127, Monsenstein und Vannerdat, 2014
  
  ► Abstract
  We summarize the contributions of the Chair for Computer Architecture at Albert-Ludwigs-Universit\"at Freiburg to the field of verification for stochastic systems. The contributions are twofold: on the one hand, there are methods for symbolic state space minimization, on the other hand efficient algorithms for counterexample generation.
• Sreedhar Saseendran Kumar, Jan Wülfing and Joschka Boedecker, Ralf Wimmer, Martin Riedmiller and Bernd Becker, Ulrich Egert: Autonomous Control of Network Activity
  Proceedings of the 9^th International Meeting on Substrate-Integrated Microelectrode Arrays (MEA), 2014
  pdf-file, BibTeX
  ► Abstract
  Electrical stimulation of the brain is used to treat neurological disorders. Yet it is unknown how to find stimulation patterns that produce desired results with the least interference. Towards this goal, we tested a generic closed-loop paradigm that autonomously optimizes stimulation settings. We used neuronal networks coupled to a reinforcement learning based controller to maximize response lengths.
• Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns: MeGARA: Menu-based Game Abstraction Refinement for Markov Automata
  Proceedings of the 12^th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), Electronic Proceedings in Theoretical Computer Science, vol. 154, pages 48–63, Open Publishing Association, 2014
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Markov automata combine continuous time, probabilistic transitions, and nondeterminism in a single model. They represent an important and powerful way to model a wide range of complex real-life systems. However, such models tend to be large and difficult to handle, making abstraction and abstraction refinement necessary. In this paper we present an abstraction and abstraction refinement technique for Markov automata, based on the game-based and menu-based abstraction of probabilistic automata. First experiments show that a significant reduction in size is possible using abstraction.
• Nils Jansen, Florian Corzilius, Matthias Volk and Ralf Wimmer, Erika Ábrahám and Joost-Pieter Katoen, Bernd Becker: Accelerating Parametric Probabilistic Verification
  Proceedings of the 11^th International Conference on Quantitative Evaluation of Systems (QEST), Lecture Notes in Computer Science, vol. 8657, pages 404–420, Springer, 2014
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We present a novel method for computing reachability probabilities of parametric discrete-time Markov chains whose transition probabilities are fractions of polynomials over a set of parameters. Our algorithm is based on two key ingredients: a graph decomposition into strongly connected subgraphs combined with a novel factorization strategy for polynomials. Experimental evaluations show that these approaches can lead to a speed-up of up to several orders of magnitude in comparison to existing approaches.
• Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer: Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
  14^th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), Advanced Lectures, Lecture Notes in Computer Science, vol. 8483, pages 65–121, Springer, 2014
  pdf-file, BibTeX , Original Publication
  ► Abstract
  This 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.
• Nils Jansen, Ralf Wimmer, Erika Ábrahám and Barna Zajzon, Joost-Pieter Katoen, Bernd Becker and Johann Schuster: Symbolic Counterexample Generation for Large Discrete-Time Markov Chains
  Science of Computer Programming, 91(A), pages 90–114, 2014
  pdf-file, BibTeX , Original Publication
  ► Abstract
  This 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$).
• Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi and Ralf Wimmer, Bernd Becker, Holger Hermanns: Abstraction-based Computation of Reward Measures for Markov Automata (extended version)
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  Markov automata allow us to model a wide range of complex real-life systems by combining continuous stochastic timing with probabilistic transitions and nondeterministic choices. By adding a reward function it is possible to model costs like the energy consumption of a system as well.
  However, models of real-life systems tend to be large, and the analysis methods for such powerful models like Markov (reward) automata do not scale well, which limits their applicability. To solve this problem we present an abstraction technique for Markov reward automata, based on stochastic games, together with automatic refinement methods for the computation of time-bounded accumulated reward properties. Experiments show a significant speed-up and reduction in system size compared to direct analysis methods.
• Ralf Wimmer, Nils Jansen, Erika Ábrahám and Joost-Pieter Katoen, Bernd Becker: Minimal Counterexamples for Linear-Time Probabilistic Verification
  Theoretical Computer Science, 549, pages 61–100, 2014
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counter\-example-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 ω-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.

2013

• Karina Gitina, Sven Reimer, Matthias Sauer and Ralf Wimmer, Christoph Scholl, Bernd Becker: Equivalence Checking of Partial Designs Using Dependency Quantified Boolean Formulae
  Proceedings of the 31^st IEEE International Conference on Computer Design, pages 396–403, IEEE Computer Society Press, 2013
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We consider the partial equivalence checking problem (PEC), i. e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied.
  Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC. We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.
• Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám: Stochastic Bounded Model Checking: Bounded Rewards and Compositionality
  Proceedings of the 16^th GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 243–254, Universität Rostock, ITMZ, 2013
  pdf-file, BibTeX
  ► Abstract
  We 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.
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker: Equivalence Checking for Partial Implementations Revisited
  Proceedings of the 16^th GI/ITG/GMM-Work\-shop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 61–70, Universität Rostock, ITMZ, 2013
  pdf-file, BibTeX
  ► Abstract
  In this paper we consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification. In particular, we investigate the relationship between the equivalence checking problem for partial implementations (PEC) and the validity problem for quantified boolean formulae (QBF) with so-called Henkin quantifiers. Our analysis leads us to a sound and complete algorithmic solution to the PEC problem as well as to an exact complexity theoretical classification of the problem.
• Ralf Wimmer, Nils Jansen, Andreas Vorpahl and Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker: High-level Counterexamples for Probabilistic Automata
  Proceedings of the 10^th International Conference on Quantitative Evaluation of Systems (QEST), Lecture Notes in Computer Science, vol. 8054, pages 18–33, Springer, 2013
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Providing 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 \textttPRISM. 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 and Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker: High-level Counterexamples for Probabilistic Automata
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  Providing 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 \textttPRISM. 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.
• Nils Jansen, Florian Corzilius, Matthias Volk and Ralf Wimmer and Erika Ábrahám, Joost-Pieter Katoen and Bernd Becker: Accelerating Parametric Probabilistic Verification
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  We present a novel method for computing reachability probabilities of parametric discrete-time Markov chains whose transition probabilities are fractions of polynomials over a set of parameters. Our algorithm is based on two key ingredients: a graph decomposition into strongly connected subgraphs combined with a novel factorization strategy for polynomials. Experimental evaluations show that combining these approaches leads to a speed-up of up to several orders of magnitude in comparison to existing approaches.

2012

• Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker: The COMICS Tool – Computing Minimal Counterexamples for DTMCs
  Proceedings of the 10^th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 7561, pages 349–353, Springer, 2012
  pdf-file, BibTeX , Original Publication
  ► Abstract
  This 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 and Erika Ábrahám and Barna Zajzon and Ralf Wimmer and Johann Schuster and Joost-Pieter Katoen and Bernd Becker: Symbolic Counterexample Generation for Discrete-time Markov Chains
  Proceedings of the 9^th International Symposium on Formal Aspects of Component Software (FACS), Lecture Notes in Computer Science, vol. 7684, pages 134–151, Springer, 2012
  pdf-file, BibTeX , Original Publication
  ► Abstract
  In 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-solving heuristics 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.
• Ralf Wimmer: Symbolische Methoden für die probabilistische Verifikation – Zustands\-raum\-reduktion und Gegenbeispiele
  Ausgezeichnete Informatikdissertationen 2011, Lecture Notes in Informatics (LNI), vol. D-12, pages 271–280, Gesellschaft für Informatik, 2012
  pdf-file, BibTeX
  ► Abstract
  Ein bekanntes Hindernis f\"ur die formale Verifikation von Systemen bildet die potentiell stark anwachsende Gr\"o\sse des Zustandsraums, genannt „Zustandsraumexplosion”. Dieses Problem konnte f\"ur digitale Schaltungen durch den Einsatz symbolischer Methoden zufriedenstellend gel\"ost oder zumindest entscheidend entsch\"arft werden. F\"ur probabilistische Systeme, die als Markow-Kette oder Markow-Entscheidungsprozess modelliert sind, brachte die direkte \"Ubertragung dieser symbolischen Methoden bisher keinen Durchbruch.
  In dieser Arbeit stellen wir zwei neue Ans\"atze vor, mit denen Markow-Modelle mit sehr gro\ssen Zustandsr\"aumen verifiziert werden k\"onnen. Die erste Methode ist ein symbolisches Verfahren zur Vorverarbeitung: Zu jedem Markow-Modell berechnen wir mit rein symbolischen Verfahren das kleinste Modell, das in den interessierenden Eigenschaften mit dem Original-Modell \"ubereinstimmt. Die Verifikation kann danach auf dem minimierten Modell durchgef\"uhrt werden. Das zweite offene Problem, das in der Dissertation gel\"ost wird, ist die symbolische Berechnung von Gegenbeispielen, wenn Sicherheitseigenschaften von Markow-Ketten mit diskreter Zeit verletzt sind. Anhand von Experimenten wird gezeigt, dass die neu entwickelten Verfahren den bisher verf\"ugbaren Verfahren hinsichtlich der Laufzeit bzw. der Gr\"o\sse der handhabbaren Systeme deutlich \"uberlegen sind.
• Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám and Joost-Pieter Katoen: Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties
  Proceedings of the 15^th GI/\allowbreak ITG/\allowbreak GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 169–180, Verlag Dr. Kova\v c, 2012
  pdf-file, BibTeX
  ► Abstract
  We propose a new approach to compute counterexamples for violated ω-regular properties of discrete-time Markov chains. 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 methods have been introduced to compute such subsystems for safety properties, based on a search for shortest paths. In this paper we use mixed integer linear programming to determine minimal critical subsystems for arbitrary ω-regular properties.
• Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen: Minimal Critical Subsystems for Discrete-Time Markov Models
  Proceedings of the 18^th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, vol. 7214, pages 299–314, Springer, 2012
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We 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, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker: The COMICS Tool – Computing Minimal Counterexamples for DTMCs
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  This report presents the tool COMICS, 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.
• Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd Becker: Transient Reward Approximation for Continuous-Time Markov Chains
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  We are interested in the analysis of very large continuous-time Markov chains (CTMCs) with many distinct rates. Such models arise naturally in the context of reliability analysis, e.g., of computer network performability analysis, of power grids, of computer virus vulnerability, and in the study of crowd dynamics. We use abstraction techniques together with novel algorithms for the computation of bounds on the expected final and accumulated rewards in continuous-time Markov decision processes (CTMDPs). These ingredients are combined in a partly symbolic and partly explicit (symblicit) analysis approach. In particular, we circumvent the use of multi-terminal decision diagrams, because the latter do not work well if facing a large number of different rates. We demonstrate the practical applicability and efficiency of the approach on two case studies.
• Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker: Minimal Counterexamples for Refuting ω-Regular Properties of Markov Decision Processes
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counter\-example-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 ω-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.

2011

• Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns and Abhishek Dhama, Oliver Theel and Ralf Wimmer, Bettina Braitling, Bernd Becker: Bounded Fairness for Probabilistic Distributed Algorithms
  Proceedings of the 11^th International Conference on Application of Concurrency to System Design (ACSD), pages 89–97, IEEE Computer Society, 2011
  pdf-file, BibTeX , Original Publication
  ► Abstract
  This paper investigates quantitative dependability metrics for distributed algorithms operating in the presence of sporadic or frequently occurring faults. In particular, we investigate necessary revisions of traditional fairness assumptions in order to arrive at useful metrics, without adding hidden assumptions that may obfuscate their validity. We formulate faulty distributed algorithms as Markov decision processes to incorporate both probabilistic faults and non-determinism arising from concurrent execution. We lift the notion of bounded fairness to the setting of Markov decision processes. Bounded fairness is particularly suited for distributed algorithms running on nearly symmetric infrastructure, as it is common for sensor network applications. Finally, we apply this fairness notion in the quantitative model-checking of several case studies.
• Nils Jansen, Erika Ábrahám, Jens Katelaan and Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker: Hierarchical Counterexamples for Discrete-Time Markov Chains
  Proceedings of the 9^th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 6996, pages 443–452, Springer, 2011
  pdf-file, BibTeX , Original Publication
  ► Abstract
  This paper introduces a novel \emphcounterexample generation approach for the verification of discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate \emphabstract counterexamples which can be refined in a \emphhierarchical manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a \emphcritical 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.
• Bettina Braitling, Ralf Wimmer, Bernd Becker and Nils Jansen, Erika Ábrahám: Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking
  Proceedings of the 13^th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS) / 31^st IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), Lecture Notes in Computer Science, vol. 6722, pages 75–89, Springer, 2011
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Generation 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.
  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.
• Bettina Braitling, Ralf Wimmer, Bernd Becker and Nils Jansen, Erika Ábrahám: SMT-based Counterexample Generation for Markov Chains
  Proceedings of the 14^th GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 19–28, Offis Oldenburg, 2011
  pdf-file, BibTeX
  ► Abstract
  Counterexamples 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.
• Ralf Wimmer, Ernst Moritz Hahn, Holger Hermanns, Bernd Becker: Reachability Analysis for Incomplete Networks of Markov Decision Processes
  Proceedings of the ACM/IEEE 9^th International Conference on Formal Methods and Models for Codesign (MEMOCODE), pages 151–160, IEEE Computer Society Press, 2011
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Assume we have a network of discrete-time Markov decision processes (MDPs) which synchronize via common actions. We investigate how to compute probability measures in case the structure of some of the component MDPs (so-called blackbox MDPs) is not known. We then extend this computation to work on networks of MDPs that share integer data variables of finite domain. We use a protocol which spreads information within a network as a case study to show the feasibility and effectiveness of our approach.
• Nils Jansen, Erika Ábrahám, Jens Katelaan and Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker: Hierarchical Counterexamples for Discrete-Time Markov Chains
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  In this paper we introduce a novel \emphcounterexample generation approach for discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate \emphabstract counterexamples, which can be refined in a \emphhierarchical manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a \emphcritical 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 orders of magnitude.

2010

• Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen and Viet Yen Nguyen, Thomas Noll, Marco Roveri and Ralf Wimmer: A Model Checker for AADL
  Proceedings of the 22^nd International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science, vol. 6174, pages 562–565, Springer, 2010
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industries for comprehensively specifying safety-critical systems by capturing functional, probabilistic and hybrid aspects. Analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment via automatic derivation of FMEA tables and dynamic fault trees, to performability evaluation, and diagnosability analysis. The toolset is currently being applied to several case studies by a major industrial developer of aerospace systems.
• Natalia Kalinnik, Erika \'Abrah\'am and Tobias Schubert, Ralf Wimmer and Bernd Becker: Exploiting Different Strategies for the Parallelization of an SMT Solver
  Proceedings of the 13^th GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 97–106, Fraunhofer-Verlag, 2010
  pdf-file, BibTeX
  ► Abstract
  In this paper we present two different parallelization schemes for the SMT solver iSAT, based on (1) the distribution of work by dividing the search space into disjoint parts and exploring them in parallel, thereby exchanging learnt information, and (2) a portfolio approach, where the entire benchmark instance is explored in parallel by several copies of the same solver but using different heuristics to guide the search. We also combine both approaches such that solvers examine disjoint parts of the search space using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT.
• Ralf Wimmer, Bernd Becker: Correctness Issues of Symbolic Bisimulation Computation for Markov Chains
  Proceedings of the 15^th International GI/ITG Conference on „Measurement, Modelling and Evaluation of Computing Systems” (MMB) and „Dependability and Fault Tolerance” (DFT), Lecture Notes in Computer Science, vol. 5987, pages 287–301, Springer, 2010
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Bisimulation reduction is a classical means to fight the infamous state space explosion problem, which limits the applicability of automated methods for verification like model checking. A signature-based method, originally developed by Blom and Orzan for labeled transition systems and adapted for Markov chains by Derisavi, has proved to be very efficient. It is possible to implement it symbolically using binary decision diagrams such that it is able to handle very large state spaces efficiently. We will show, however, that for Markov chains this algorithm suffers from numerical instabilities, which often result in too large quotient systems. We will present and experimentally evaluate two different approaches to avoid these problems: first the usage of rational arithmetic, and second an approach not only to represent the system structure but also the transition rates symbolically. In addition, this allows us to modify their actual values after the quotient computation.
• Erika Ábrahám, Ulrich Loup, Ralf Wimmer, Joost-Pieter Katoen: On the Minimization of Hybrid Automata
  Proceedings of the 22^nd Nordic Workshop on Programming Theory (NWPT), 2010
  
  ► Abstract
  Minimization is a widely used technique for the abstraction of systems with large or infinite state spaces. The result of the minimization is a finite partitioning of the concrete state space and an induced abstract transition system with the partitions as abstract states. This final abstract transition system is bisimilar to the concrete system with respect to the reachable states and the observable actions.
  In this work we discuss the minimization of hybrid systems and introduce a modified minimization algorithm. It computes an abstraction that is in general not bisimilar to the concrete system, but it provides enough information for reachability analysis. Furthermore, besides the well-known forward approach for minimization, we discuss as an alternative a backward minimization method.
• Ralf Wimmer, Salem Derisavi, Holger Hermanns: Symbolic Partition Refinement with Automatic Balancing of Time and Space
  Performance Evaluation, 67(9), pages 815–835, 2010
  pdf-file, BibTeX , Original Publication
  ► Abstract
  State space lumping is one of the classical means to fight the state space explosion problem in state-based performance evaluation and verification. Particularly when numerical algorithms are applied to analyze a Markov model, one often observes that those algorithms do not scale beyond systems of moderate size. To alleviate this problem, symbolic lumping algorithms have been devised to effectively reduce very large–-but symbolically represented–-Markov models to moderate size explicit representations. This lumping step partitions the Markov model in such a way that any numerical analysis carried out on the lumped model is guaranteed to produce exact results for the original system. But even this lumping preprocessing may fail due to time or memory limitations. This paper discusses the two main approaches to symbolic lumping, and combines them to improve on their respective limitations. The algorithm automatically converts between known symbolic partition representations in order to provide a trade-off between memory consumption and runtime. We show how to apply this algorithm for the lumping of Markov chains, but the same techniques can be adapted in a straightforward way to other models like Markov reward models, labeled transition systems, or interactive Markov chains.
• Ralf Wimmer, Bettina Braitling, Bernd Becker and Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns and Abhishek Dhama, Oliver Theel: Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems
  Proceedings of the 7^th International Conference on Quantitative Evaluation of Systems (QEST), pages 27–36, IEEE Computer Society Press, 2010
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Model checkers for concurrent probabilistic systems have become very popular within the last decade. The study of long-run average behavior has however received only scant attention in this area, at least from the implementation perspective. This paper studies the problem of how to efficiently realize an algorithm for computing optimal long-run average reward values for concurrent probabilistic systems. At its core is a variation of Howard and Veinott's algorithm for Markov decision processes, where symbolic and non-symbolic representations are intertwined in an effective manner: the state space is represented using binary decision diagrams, while the linear equation systems which have to be solved for the induced Markov chains to improve the current scheduler are solved using an explicit state representation. In order to keep the latter small, we apply a symbolic bisimulation minimization algorithm to the induced Markov chain. The scheduler improvement step itself is again performed on symbolic data structures. Practical evidence shows that the implementation is effective, and sometimes uses considerably less memory than a fully explicit implementation.
• Erika Ábrahám , Nils Jansen and Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker: DTMC Model Checking by SCC Reduction
  Proceedings of the 7^th International Conference on Quantitative Evaluation of Systems (QEST), pages 37–46, IEEE Computer Society Press, 2010
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Discrete-Time Markov Chains (DTMCs) are a widely-used formalism to model probabilistic systems. On the one hand, available tools like Prism or Mrmc offer efficient \emphmodel checking algorithms and thus support the verification of DTMCs. However, these algorithms do not provide any diagnostic information in the form of \emphcounterexamples, which are highly important for the correction of erroneous systems. On the other hand, there exist several approaches to generate counterexamples for DTMCs, but all these approaches require the model checking result for completeness.
  In this paper we introduce a model checking algorithm for DTMCs that also supports the generation of counterexamples. Our algorithm, based on the detection and abstraction of strongly connected components, offers \emphabstract counterexamples, which can be interactively refined by the user.
• Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns and Abhishek Dhama, Oliver Theel and Ralf Wimmer, Bettina Braitling, Bernd Becker: Bounded Fairness for Probabilistic Distributed Algorithms
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  This paper investigates quantitative dependability metrics for distributed algorithms operating in the presence of sporadic or frequently occurring faults. In particular, we investigate necessary revisions of traditional fairness assumptions in order to arrive at useful metrics, without adding hidden assumptions that may obfuscate their validity. We formulate distributed algorithms as Markov decision processes to incorporate both probabilistic faults and non-determinism arising from the distributed setting. We especially discuss the notions of bounded fairness and near-round-robin schedulers, which appear particularly suited for distributed algorithms running on nearly symmetric infrastructure, as it is common for sensor network applications. We further develop methods to incorporate this fairness notion in the quantitative model checking of distributed algorithms. Finally, we apply our methodology to several case studies to provide a first experimental insight into its applicability.

2009

• Natalia Kalinnik, Tobias Schubert and Erika Ábrahám and Ralf Wimmer and Bernd Becker: Picoso – A Parallel Interval Constraint Solver
  Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA), pages 473–479, CSREA Press, 2009
  pdf-file, BibTeX
  ► Abstract
  This paper describes the \underlineparallel \underlineinterval \underlineconstraint \underlinesolver Picoso, which can decide (a subclass of) boolean combinations of linear and non-linear constraints. Picoso follows a master/client model based on message passing, making it suitable for any kind of workstation cluster as well as for multi-processor machines. To run several clients in parallel, an efficient work stealing mechanism has been integrated, dividing the overall search space into disjoint parts. Additionally, to prevent the clients from running into identical conflicts, information about conflicts in form of conflict clauses is exchanged among the clients. Performance measurements, using four clients to solve a number of benchmark problems, show that Picoso yields linear speedup compared to the sequential interval constraint solver iSAT, on which the clients of Picoso are based.
• Abhishek Dhama, Oliver Theel and Pepijn Crouzen, Holger Hermanns and Ralf Wimmer, Bernd Becker: Dependability Engineering of Silent Self-Stabilizing Systems
  Proceedings of the 11^th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), Lecture Notes in Computer Science, vol. 5873, pages 238–253, Springer, 2009
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Self-stabilization is an elegant way of realizing non-masking fault-tolerant systems. Sustained research over last decades has produced multiple self-stabilizing algorithms for many problems in distributed computing. In this paper, we present a framework to evaluate multiple self-stabilizing solutions under a fault model that allows intermittent transient faults. To that end, metrics to quantify the dependability of self-stabilizing systems are defined. It is also shown how to derive models that are suitable for probabilistic model checking in order to determine those dependability metrics. A heuristics-based method is presented to analyze counterexamples returned by a probabilistic model checker in case the system under investigation does not exhibit the desired degree of dependability. Based on the analysis, the self-stabilizing algorithm is subsequently refined.
• Eckard Böde, Marc Herbstritt and Holger Hermanns and Sven Johr and Thomas Peikenkamp, Reza Pulungan and Jan-Hendrik Rakow and Ralf Wimmer and Bernd Becker: Compositional Dependability Evaluation for Statemate
  IEEE Transactions on Software Engineering, 35(2), pages 274–292, 2009
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Software and system dependability is getting ever more important in embedded system design. Current industrial practice of model-based analysis is supported by state-transition diagrammatic notations such as Statecharts. State-of-the-art modelling tools like Statemate support safety and failure-effect analysis at design time, but restricted to qualitative properties. This paper reports on a (plug-in) extension of Statemate enabling the evaluation of quantitative dependability properties at design time. The extension is compositional in the way the model is augmented with probabilistic timing information. This fact is exploited in the construction of the underlying mathematical model, a uniform continuous-time Markov decision process, on which we are able to check requirements of the form: \emph„The probability to hit a safety-critical system configuration within a mission time of 3 hours is at most 0.01.” We give a detailed explanation of the construction and evaluation steps making this possible, and report on a nontrivial case study of a high-speed train signalling system where the tool has been applied successfully.
• Ralf Wimmer, Bettina Braitling, Bernd Becker: Counterexample Generation for Discrete-time Markov Chains using Bounded Model Checking
  Proceedings of the 10^th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Lecture Notes in Computer Science, pages 366–380, Springer, 2009
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Since its introduction in 1999, bounded model checking has gained industrial relevance for detecting errors in digital and hybrid systems. One of the main reasons for this is that it always provides a counterexample when an erroneous execution trace is found. Such a counterexample can guide the designer while debugging the system.
  In this paper we are investigating how bounded model checking can be applied to generate counterexamples for a different kind of model–-namely discrete-time Markov chains. Since in this case counterexamples in general do not consist of a single path to a safety-critical state, but of a potentially large set of paths, novel optimization techniques like loop-detection are applied not only to speed-up the counterexample computation, but also to reduce the size of the counterexamples significantly. We report on some experiments which demonstrate the practical applicability of our method.

2008

• Ralf Wimmer and Alexander Kortus and Marc Herbstritt and Bernd Becker: Probabilistic Model Checking and Reliability of Results
  Proceedings of the 11^th IEEE International Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS), pages 207–212, IEEE Computer Society Press, 2008
  pdf-file, BibTeX , Original Publication
  ► Abstract
  In formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations of the model checking algorithms due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.
  We motivate our investigations with an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. We then analyze, at which points inaccuracies are introduced during the model checking process. We discuss first ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential correctness problems: (1) usage of exact (rational) arithmetic, (2) usage of interval arithmetic to obtain safe approximations of the actual probabilities, (3) provision of certificates which testify that the result is correct, and (4) integration of a „degree of belief” for each sub-formula into existing model checking tools.
• Bernd Becker and Marc Herbstritt and Natalia Kalinnik and Matthew Lewis and Juri Lichtner and Tobias Nopper and Ralf Wimmer: Propositional Approximations for Bounded Model Checking of Partial Circuit Designs
  Proceedings of the 26^th IEEE International Conference on Computer Design (ICCD), pages 52–59, IEEE Computer Society Press, 2008
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Bounded model checking of partial circuit designs enables the detection of errors even when the implementation of the design is not finished. The behavior of the missing parts can be modeled by a conservative extension of propositional logic, called 01X-logic. Then the transitions of the underlying (incomplete) sequential circuit under verification have to be represented adequately. In this work, we investigate the difference between a relation-oriented and a function-oriented approach for this issue. Experimental results on a large set of examples show that the function-oriented representation is most often superior w. r. t. (1) CPU runtime and (2) accuracy regarding the ability to find a counterexample, such that by using the function-oriented approach an increase of accuracy up to 210\% and a speed-up of the CPU runtime up to 390\% compared to the relation-oriented approach are achieved. But there are also relevant examples, e. g. a VLIW-ALU, for which the relation-oriented approach outperforms the function-oriented one by 300\% in terms of CPU-time, showing that both approaches are efficient for different scenarios.
• Ralf Wimmer, Alexander Kortus and Marc Herbstritt, Bernd Becker: The Demand for Reliability in Probabilistic Verification
  Proceedings of the 11^th GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 99–108, Shaker-Verlag, 2008
  pdf-file, BibTeX
  ► Abstract
  For formal verification, reliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations due to logical errors are the source of wrong results. In probabilistic model checking, however, numerical instabilities are an additional source for inconsistent results.
  First we present an example, for which several state-of-the-art probabilistic model checking tools give completely wrong results due to inexact computations. This motivates the investigation at which points inaccuracies are introduced during the model checking process. We then give ideas how, in spite of these inaccuracies, reliable results can be obtained or at least the user be warned about potential problems: (1) to introduce a „degree of belief” for each sub-formula, (2) to use exact (rational) arithmetic, (3) to use interval arithmetic to obtain safe approximations of the actual probabilities, and (4) to provide certificates which testify that the result is correct.
• Ralf Wimmer, Salem Derisavi, Holger Hermanns: Symbolic Partition Refinement with Dynamic Balancing of Time and Space
  Proceedings of the 5^th International Conference on Quantitative Evaluation of Systems (QEST), pages 65–74, IEEE Computer Society Press, 2008
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Bisimulation minimization is one of the classical means to fight the infamous state space explosion problem in verification. Particularly in stochastic verification, numerical algorithms are applied, which do not scale beyond systems of moderate size. To alleviate this problem, symbolic bisimulation minimization has been used effectively to reduce very large symbolically represented state spaces to moderate size explicit representations. But even this minimization may fail due to time or memory limitations. This paper presents a symbolic algorithm which relies on a hybrid symbolic partition representation. It dynamically converts between two known representations in order to provide a trade-off between memory consumption and runtime. The conversion itself is logarithmic in the partition size. We show how to apply it for the minimization of Markov chains, but the same techniques can be adapted in a straightforward way to other models like labeled transition systems or interactive Markov chains.

2007

• Ralf Wimmer, Marc Herbstritt, Bernd Becker: Optimization Techniques for BDD-based Bisimulation Minimization
  Proceedings of the 17^th ACM Great Lakes Symposium on VLSI (GLSVLSI), pages 405–410, ACM Press, 2007
  pdf-file, BibTeX , Original Publication
  ► Abstract
  In this paper we report on optimizations for a BDD-based algorithm for the computation of bisimulations. The underlying algorithmic principle is an iterative refinement of a partition of the state space. The proposed optimizations demonstrate that both, taking into account the algorithmic structure of the problem and the exploitation of the BDD-based representation, are essential to finally obtain an efficient symbolic algorithm for real-world problems. The contributions of this paper are (1) block forwarding to update block refinement as soon as possible, (2) split-driven refinement that over-approximates the set of blocks that must definitely be refined, and (3) block ordering to fix the order of the blocks for the refinement in a clever way. We provide substantial experimental results on examples from different applications and compare them to alternative approaches when possible. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches.
• Ralf Wimmer, Marc Herbstritt, Bernd Becker: Forwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation
  Proceedings of the 10^th GI/ITG/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 203–212, Shaker-Verlag, 2007
  pdf-file, BibTeX
  ► Abstract
  In this paper we present optimizations for a BDD-based algorithm for the computation of several types of bisimulations which play an important role for minimisation of large systems thus enabling their verification. The basic principle of the algorithm is partition refinement. Our proposed optimizations take this refinement-structure as well as the usage of BDDs for the representation of the system into account: (1) \emphblock forwarding updates in-situ newly refined blocks of the partition, (2) \emphsplit-driven refinement approximates the blocks that may be refined, and (3) \emphblock ordering heuristically suggests a good order in which the blocks will be refined.
  We provide substantial experimental results on examples from different applications and compare them to alternative approaches. The experiments clearly show that the proposed optimization techniques result in a significant performance speed-up compared to the basic algorithm as well as to alternative approaches.
• Ralf Wimmer, Holger Hermanns and Marc Herbstritt and Bernd Becker: Towards Symbolic Stochastic Aggregation
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  Bisimulations are one of the classical means to fight the state explosion problem. Especially in combination with symbolic methods, like BDD-based data representation and algorithms that exploit the compact BDD representation, they enable the minimization of very large state spaces without losing relevant properties. In this report, we show how a symbolic algorithm, that was originally developed for non-stochastic systems, can be extended to compute strong and branching bisimulations on interactive Markov chains (IMCs). An IMC is a very general model that combines the stochastic behavior of traditional Markov chains with action-labeled transition systems. To the best of our knowledge, our suggested algorithm is the first symbolic algorithm for both stochastic \emphstrong bisimulation and stochastic \emphbranching bisimulation on IMCs.
• Ralf Wimmer, Alexander Kortus and Marc Herbstritt and Bernd Becker: Symbolic Model Checking for DTMCs with Exact and Inexact Arithmetic
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  In formal verification, \emphreliable results are of utmost importance. In model checking of digital systems, mainly incorrect implementations due to logical errors are the source of wrong results. In probabilistic model checking, numerical instabilities are an additional source for inconsistent results. In this report, we experimentally analyze the impact of inexact floating-point arithmetic on the correctness of the result in the context of probabilistic model checking of discrete-time Markov chains. Inexact arithmetic performs implicitly \emphrounding of values that are generated during the model checking process. To enable a direct comparison to the state of the art, which relies on inexact floating-point arithmetic, we have implemented a prototypical probabilistic model checker that provides standard floating-point arithmetic as well as exact arithmetic. During our experimental evaluation, we found practical examples where the use of inexact arithmetic produces unacceptable results. Two reasons for these problems are: (1) Rounding can change the structure of the system, and (2) rounding can change the truth-value of sub-formulae. Both issues can result in probabilities that are far away from the correct ones. As a summary, this work reveals the demand for investigating reliable numerical methods within probabilistic model checking.

2006

• Ralf Wimmer, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker: Sigref – A Symbolic Bisimulation Tool Box
  Proceedings of the 4^th International Symposium on Automated Technology for Verification and Analysis (ATVA), Lecture Notes in Computer Science, vol. 4218, pages 477–492, Springer, 2006
  pdf-file, BibTeX , Original Publication
  ► Abstract
  We present a uniform signature-based approach to compute the most popular bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large transition systems. Signatures for the bisimulations are built up from a few generic building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate signature is the key for a rapid development of algorithms for other types of bisimulation. We provide experimental evidence of the viability of this approach by presenting computational results for many bisimulations on real-world instances. The experiments show cases where our framework can handle state spaces efficiently that are far too large to handle for any tool that requires an explicit state space description.
• Ralf Wimmer, Marc Herbstritt, Bernd Becker: Minimization of Large State Spaces using Symbolic Branching Bisimulation
  Proceedings of the 9^th IEEE International Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS), pages 9–14, IEEE Computer Society Press, 2006
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Bisimulations in general are a powerful concept to minimize large finite state systems regarding some well-defined observational behavior. In contrast to strong bisimulation, for branching bisimulation there are only tools available that work on an explicit state space representation. In this work we present for the first time a symbolic approach for branching bisimulation that uses BDDs as basic data structure and that is based on the concept of signature refinement. First experimental results for problem instances derived from process algebraic system descriptions show the feasibility and the robustness of our approach.
• Ralf Wimmer, Tobias Nopper, Marc Herbstritt and Christoph Löffler, Bernd Becker: Collaborative Exercise Management
  Proceedings of the 11^th World Conference on E-Learning in Corporate, Government, Health Care, & Higher Education (E-Learn), pages 3127–3134, Association for the Advancement of Computers in Education (AACE), 2006
  pdf-file, BibTeX
  ► Abstract
  In this work, we report on a novel tool for managing exercises used in a collaborative course organization environment at university. Our approach focuses on the separation of the content of the exercises and its layout. The latter is based on the typesetting system \LaTeX. Content management of the exercises is established by a web-based interface. As a whole, our tool provides a time-saving and unambiguous workflow for collaborative, time- and place-independent exercise organization.
• Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd Becker: Compositional Performability Evaluation for Statemate
  Proceedings of the 3^rd International Conference on Quantitative Evaluation of Systems (QEST), IEEE Computer Society Press, 2006
  pdf-file, BibTeX , Original Publication
  ► Abstract
  This paper reports on our efforts to link an industrial state-of-the-art modelling tool to academic state-of-the-art analysis algorithms. In a nutshell, we enable timed reachability analysis of uniform continuous-time Markov decision processes, which are generated from Statemate models. We give a detailed explanation of several construction, transformation, reduction, and analysis steps required to make this possible. The entire tool flow has been implemented, and it is applied to a nontrivial example.
• Marc Herbstritt, Ralf Wimmer, Thomas Peikenkamp, Eckard Böde, Michael Adelaide, Sven Johr, Holger Hermanns, Bernd Becker: Analysis of Large Safety-Critical Systems: A quantitative Approach
  Technical report.
  pdf-file, BibTeX
  ► Abstract
  The ever increasing complexity of systems requires combined efforts with respect to analysis and verification to close the so-called verification gap. On the modeling side, to face this problem, expressive high-level methodologies are used to manage system complexity. From the analysis side it is therefore essential to also start at this level. Due to powerful symbolic tools – often based on BDDs – consistent high-level representations can be generated. The bottleneck for subsequent system analysis, however, is still the incredible state space of such representations. This fact gains even more importance when the intended analysis is bound to explicit tools, e.g.,~for a quantitative analysis using stochastic model checking. In this work, we are bridging the gaps between high-level system descriptions of safety-critical systems and corresponding explicit state space representations that can be handled by explicit quantitative analysis tools. In a first step, our approach safely integrates failure behavior of safety-critical systems into their high-level description. Then, structural reductions are applied. Manageable explicit representations are finally obtained by a novel BDD-based symbolic branching bisimulation algorithm. We provide experimental data demonstrating the efficiency of our methods: safety-critical systems whose size seems to be prohibitive for any explicit analysis tool at the beginning are reduced by orders of magnitude, thus paving the way to quantitative analysis without losing relevant information.

2005

• Bernd Becker, Markus Behle, Friedrich Eisenbrand, Ralf Wimmer: BDDs in a Branch & Cut Framework
  Proceedings of the 4^th International Workshop on Efficient and Experimental Algorithms (WEA), Lecture Notes in Computer Science, vol. 3503, pages 452–463, Springer, 2005
  pdf-file, BibTeX , Original Publication
  ► Abstract
  Branch & Cut is today's state-of-the-art method to solve 0/1-integer linear programs. Important for the success of this method is the generation of strong valid inequalities, which tighten the linear programming relaxation of 0/1-IPs and thus allow for early pruning of parts of the search tree.
  In this paper we present a novel approach to generate valid inequalities for 0/1-IPs which is based on Binary Decision Diagrams (BDDs). BDDs are a datastructure which represents 0/1-vectors as paths of a certain acyclic graph. They have been successfully applied in computational logic, hardware verification and synthesis.
  We implemented our BDD cutting plane generator in a branch-and-cut framework and tested it on several instances of the MAX-ONES problem and randomly generated 0/1-IPs. Our computational results show that we have developed competitive code for these problems, on which state-of-the-art MIP-solvers fall short.

2004

• Bernd Becker, Markus Behle, Friedrich Eisenbrand, Martin Fränzle and Marc Herbstritt, Christian Herde, Jörg Hoffmann, Daniel Kröning, Bernhard Nebel, Ilia Polian, Ralf Wimmer: Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
  Proceedings of the 7^th ITG/GI/GMM-Workshop „Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” (MBMV), pages 65–75, Shaker-Verlag, 2004
  pdf-file, BibTeX
  ► Abstract
  We present a concept to significantly advance the state of the art for bounded model checking (BMC) and inductive verification (IV) of hybrid discrete-continuous systems. Our approach combines the expertise of partners coming from different domains, like hybrid systems modeling and digital circuit verification, bounded planning and heuristic search, combinatorial optimization and integer programming. After sketching the overall verification flow we present first results indicating that the combination and tight integration of different verification engines is a first step to pave the way to fully automated BMC and IV of medium to large-scale networks of hybrid automata.