2021

 nach oben zur Jahresübersicht

• Pascal Pieper, Ralf Wimmer, Gerhard Angst, Rolf Drechsler
  Minimally Invasive HW/SW Co-debug Live Visualization on Architecture Level
  2021 ACM Press
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2020

 nach oben zur Jahresübersicht

• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker
  Strategy Synthesis for POMDPs in Robot Planning using Game-Based Abstractions
  2020 IEEE T Automat Contr
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Leonore Winterer, Ralf Wimmer, Nils Jansen, Bernd Becker
  Strengthening Determinstic Policies for POMPDs
  2020 Proceedings of the 12th NASA Formal Methods Symposium (NFM)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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

 nach oben zur Jahresübersicht

• Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst
  A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving
  2019 Honolulu, HI, USA Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI), AAAI Press
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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^P 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.
• Steven Carr, Nils Jansen, Ralf Wimmer, Alexandru Constantin Serban, Bernd Becker, Ufuk Topcu
  Counterexample-Guided Strategy Improvement for POMDPs using Recurrent Neural Networks
  2019 Macao, China Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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
  Localizing Quantifiers for DQBF
  2019 Proceedings of the 2019 Conference on Formal Methods in Computer Aided Design (FMCAD), Clark W. Barrett, Jin Yang
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Ralf Wimmer, Christoph Scholl, Bernd Becker
  The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation
  2019 Journal on Satisfiability, Boolean Modeling and Computation, Band: 11, Nummer: 1, Seiten: 3 - 52
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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 that 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.

2018

 nach oben zur Jahresübersicht

• Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Kaoten, Becker B
  Abstraktions-basierte Verifikation von POMDPs im Motion-Planning-Kontext
  2018 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Wir untersuchen Pfadplanungsprobleme aus der Robotik und die Berechnung von Stra- tegien, 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 na- tü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.
• Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker
  Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas
  In: Advanced Logic Synthesis
  2018, Springer, André Ignacio Reis and Rolf Drechsler, Seiten: 151 - 168, André Ignacio Reis and Rolf Drechsler, ISBN: 978-3-319-67294-6
• Christoph Scholl, Ralf Wimmer
  Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
  2018 Oxford, UK Proceedings of the 21st Int'l Conf. on Theory and Applications of Satisfiability Testing (SAT), Olaf Beyersdorff, Christoph M. Wintersteiger, Band: 10929, Seiten: 3 - 16
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker
  Finite-State Controllers of POMDPs via Parameter Synthesis
  2018 Proceedings of the 34th Conference on Uncertainty in Artificial Intelligence (UAI), AUAI Press, Seiten: 519 - 529
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  e 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.
• Steven Carr, Nils Jansen, Ralf Wimmer, Jie Fu, Ufuk Topcu
  Human-in-the-Loop Synthesis for Partially Observable Markov Decision Processes
  2018 Proceedings of the 2018 Annual American Control Conference (ACC), Seiten: 762 - 69
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Yuliya Butkova, Ralf Wimmer, Holger Hermanns
  Markov Automata on Discount!
  2018 19. International GI/ITG Conference on Measurement, Modelling and Evaluation of Computing Systems (MMB), Reinhard German et al., Band: 10740
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2017

 nach oben zur Jahresübersicht

• Hassan Hatefi, Ralf Wimmer, Bettina Braitling, Luis Maria Ferrer Fioriti, Bernd Becker, Holger Hermanns
  Cost vs. Time in Stochastic Games and Markov Automata
  2017 Form Asp Comput, Band: 29, Nummer: 4, Seiten: 629 - 649
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker
  From DQBF to QBF by Dependency Elimination
  2017 Melbourne, VIC, Australia Int'l Conf. on Theory and Applications of Satisfiability Checking, Serge Gaspers and Toby Walsh, Band: 10491, Seiten: 326 - 343
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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
  2017 Uppsala, Sweden International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I, Axel Legay and Tiziana Margaria, Band: 10205, Seiten: 373 - 390
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present our new preprocessor \textsc{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
  2017 Uppsala, Sweden International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part II, Axel Legay and Tiziana Margaria, Band: 10206, Seiten: 188 - 203
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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, Ufuk Topcu, Joost-Pieter Kaoten, Becker B
  Motion Planning under Partial Observability using Game-Based Abstraction
  2017 Melbourne, VIC, Australia 56th IEEE Conf. on Decision and Control (CDC), Seiten: 2201 - 2208
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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 evironment. 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, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker
  Permissive Finite-State Controllers of POMDPs using Parameter Synthesis
  2017
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Bernd Becker, Christoph Scholl, Ralf Wimmer
  Verification of Incomplete Designs
  In: Formal System Verification - State of the Art and Future Trends
  2017, Springer, Rolf Drechsler, Seiten: 37 - 72, Rolf Drechsler, ISBN: 978-3-319-57683-1
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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?'').

2016

 nach oben zur Jahresübersicht

• Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker
  Dependency Schemes for DQBF
  2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Band: 9710, Seiten: 473 - 489
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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
  2016 Int'l Symposium on Automated Technology for Verification and Analysis (ATVA) Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA), Springer, Band: 9938, Seiten: 395 - 411
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Skolem Functions for DQBF (Extended Version)
  , 2016
• Ralf Wimmer
  Tagungsband des 19. GI/ITG/GMM-Workshops "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV)
  2016 Universität Freiburg / FreiDok, Seite: 150

2015

 nach oben zur Jahresübersicht

• Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns
  Abstraction-based Computation of Reward Measures for Markov Automata
  2015 Mumbai, India Int'l Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI), Band: 8931, Seiten: 172 - 189
• Hassan Hatefi, Bettina Braitling, Ralf Wimmer, Luis Maria Ferrer Fioriti, Holger Hermanns, Bernd Becker
  Cost vs. Time in Stochastic Games and Markov Automata
  2015 International Symposium on Dependable Software Engineering: Theory, Tools and Applications (SETTA) Proc. of SETTA, Springer-Verlag, Band: 9409, Seiten: 19 - 34
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
  Counterexamples for Expected Rewards
  2015 Proceedings of the 20th International Symposium on Formal Methods (FM), Springer, Band: 9109, Seiten: 435 - 452
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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
  2015 Log Meth Comput Sci (Logical Methods In Computer Science), Band: 11, Nummer: 1:15, Seiten: 1 - 23
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Bernd Becker, Matthias Sauer, Christoph Scholl, Ralf Wimmer
  Modeling Unknown Values in Test and Verification
  In: Formal Modeling and Verification of Cyber-Physical Systems (Proceedings of the 1st International Summer School on Methods and Tools for the Design of Digital Systems)
  2015, Springer, Rolf Drechsler, Ulrich Kühne, Seiten: 122 - 150, Rolf Drechsler, Ulrich Kühne, ISBN: 978-3-658-09993-0
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  mbination 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.
• Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker
  Preprocessing for DQBF
  2015 Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Band: 9340, Seiten: 173 - 190
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker
  Solving DQBF Through Quantifier Elimination
  2015 Conf. on Design, Automation and Test in Europe
• Karsten Scheibler, Leonore Winterer, Ralf Wimmer, Bernd Becker
  Towards Verification of Artificial Neural Networks
  2015 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd Becker
  Transient Reward Approximation for Continuous-Time Markov Chains
  2015 Ieee T Reliab, Band: 64, Nummer: 4
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2014

 nach oben zur Jahresübersicht

• Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  Accelerating Parametric Probabilistic Verification
  2014 Int'l Conf. on Quantitative Evaluation of Systems (QEST), Springer-Verlag, Band: 8657, Seite: 404-420
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Sreedhar Saseendran Kumar, Jan Wülfing, Joschka Boedecker, Ralf Wimmer, Martin Riedmiller, Bernd Becker, Ulrich Egert
  Autonomous Control of Network Activity
  2014 9th International Meeting on Substrate-Integrated Microelectrode Arrays (MEA)
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Erika Ábrahám, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer
  Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey
  In: International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM), Advanced Lectures
  2014, Springer-Verlag, Seiten: 65 - 121,
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
  Fast Debugging of PRISM Models
  2014 Int'l Symp. on Automated Technology for Verfication and Analysis, Springer-Verlag
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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
  In: Aspekte der Technischen Informatik: Festschrift zum 60. Geburtstag von Bernd Becker
  2014, Monsenstein und Vannerdat, Rolf Drechsler, Seiten: 119 - 127, Rolf Drechsler,
• Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger Hermanns
  MeGARA: Menu-based Game Abstraction and Abstraction Refinement of Markov Automata
  2014 International Workshop on Quantitative Aspects of Programming Languages and Systems , Band: EPTCS
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  abstraction.
• Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  Minimal Counterexamples for Linear-Time Probabilistic Verification
  2014 Theor Comput Sci
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Counterexamples for property violations have a number of important applications like supporting the debugging of erroneous systems and verifying large systems via counterexample-guided abstraction refinement. In this paper, we propose the usage of minimal critical subsystems of discrete-time Markov chains and Markov decision processes as counterexamples for violated omega-regular properties. Minimality can thereby be defined in terms of the number of states or transitions. This problem is known to be NP-complete for Markov decision processes. We show how to compute such subsystems using mixed integer linear programming and evaluate the practical applicability in a number of experiments. They show that our method yields substantially smaller counterexample than using existing techniques.
• Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster
  Symbolic Counterexample Generation for Large Discrete-Time Markov Chains
  2014 Sci Comput Program, Band: 91, Nummer: A, Seiten: 90 - 114
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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}).

2013

 nach oben zur Jahresübersicht

• Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Becker, Bernd
  Accelerating Parametric Probabilistic Verification
  arXiv, Band: arXiv:1312.3979, 2013
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking for Partial Implementations Revisited
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Universität Rostock ITMZ, Seiten: 61 - 70
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking of Partial Designs using Dependency Quantified Boolean Formulae
  2013 Int'l Conf. on Computer Design, IEEE Computer Society, Seiten: 396 - 403
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  High-Level Counterexamples for Probabilistic Automata
  2013 Springer-Verlag, Band: 8054, Seiten: 18 - 33
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  simplified to obtain a well-understandable counterexample.
• Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  High-Level Counterexamples for Probabilistic Automata
  , Band: arxiv:1305.5055, 2013
• Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Ábrahám
  Stochastic Bounded Model Checking: Bounded Rewards and Compositionality
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Seiten: 243 - 254
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  cases.

2012

 nach oben zur Jahresübersicht

• Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
  Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
  AVACS Technical Report, Nummer: 88, 2012
• Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
  Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties
  2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Verlag Dr. Kovac, Seiten: 169 - 180
• Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
  Minimal Critical Subsystems for Discrete-Time Markov Models
  2012 Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Springer-Verlag, Band: 7214, Seiten: 299 - 314
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker
  Symbolic Counterexample Generation for Discrete-time Markov Chains
  2012 Int'l Symp. on Formal Aspects of Component Software, Springer-Verlag, Band: 7684, Seiten: 134 - 151
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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-solvingheuristics to prefer paths with higher probabilities. As a second approach, we use symbolic graph algorithms to find counterexamples. Experiments show that our approaches, in contrast to other existing techniques, are applicable to very large systems with millions of states.
• Ralf Wimmer
  Symbolische Methoden für die probabilistische Verifikation
  In: Ausgezeichnete Informatik-Dissertationen
  2012, Gesellschaft für Informatik, Stefan Hölldobler et al., Seiten: 271 - 280, Stefan Hölldobler et al., ISBN: 978-3-88579-416-5
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Laufzeit bzw. der Größe der handhabbaren Systeme deutlich überlegen sind.
• Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  The COMICS Tool - Computing Minimal Counterexamples for DTMCs
  2012 Automated Technology for Verification and Analysis, Springer-Verlag, Band: 7561, Seiten: 349 - 353
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  The COMICS Tool - Computing Minimal Counterexamples for DTMCs
  , Band: arxiv:1206.0603, 2012
• Ernst Moritz Hahn, Holger Hermanns, Ralf Wimmer, Bernd Becker
  Transient Reward Approximation for Grids, Crowds, and Viruses
  arXiv, Band: arxiv:1212.1251, 2012

2011

 nach oben zur Jahresübersicht

• Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver Theel, Ralf Wimmer, Bettina Braitling, Bernd Becker
  Bounded Fairness for Probabilistic Distributed Algorithms
  2011 Int'l Conf. on Application of Concurrency to System Design, IEEE Computer Society, Seiten: 89 - 97
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
  Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking
  2011 IFIP Int'l Conf. on Formal Methods for Open Object-based Distributed Systems, Springer-Verlag, Band: 6722, Seiten: 75 - 89
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.\par In this paper we introduce the usage of SMT-solving over linear real arithmetic for the BMC procedure. SMT-solving, extending SAT with theories in this context on the one hand leads to a convenient way to express conditions on the probability of certain paths and on the other hand allows to handle Markov reward models. We use the former to find paths with high probability first. This leads to more compact counterexamples. We report on some experiments, which show promising results.
• Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  Hierarchical Counterexamples for Discrete-Time Markov Chains
  2011 Int'l Symp. on Automated Technology for Verification and Analysis, Springer-Verlag, Band: 6996, Seiten: 443 - 452
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper introduces a novel counterexample generation approach for the verification of discrete-time Markov chains (DTMCs) with two main advantages: (1) We generate abstract counterexamples which can be refined in a hierarchical manner. (2) We aim at minimizing the number of states involved in the counterexamples, and compute a critical subsystem of the DTMC whose paths form a counterexample. Experiments show that with our approach we can reduce the size of counterexamples and the number of computation steps by several orders of magnitude.
• Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  Hierarchical Counterexamples for Discrete-Time Markov Chains
  , Band: AIB-2011-11, 2011
• Ralf Wimmer, Ernst Moritz Hahn, Holger Hermanns, Bernd Becker
  Reachability Analysis for Incomplete Networks of Markov Decision Processes
  2011 Int'l Conf. on Formal Methods and Models for Co-Design, IEEE Computer Society Press, Seiten: 151 - 160
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Ábrahám
  SMT-based Counterexample Generation for Markov Chains
  2011 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Offis Oldenburg, Band: 14, Seiten: 19 - 28
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2010

 nach oben zur Jahresübersicht

• Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer
  A Model Checker for AADL
  2010 Int'l Conf. on CAV, Springer-Verlag, Band: 6174, Seiten: 562 - 565
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  We present a graphical toolset for verifying AADL models, which aregaining widespread acceptance in aerospace, automobile and avionicsindustries for comprehensively specifying safety-critical systems bycapturing functional, probabilistic and hybrid aspects. Analysesare implemented on top of mature model checking tools and range fromrequirements validation to functional verification, safety assessmentvia automatic derivation of FMEA tables and dynamic fault trees,to performability evaluation, and diagnosability analysis. The toolset iscurrently being applied to several case studies by a major industrialdeveloper of aerospace systems.
• Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver Theel, Ralf Wimmer, Bettina Braitling, Bernd Becker
  Bounded Fairness for Probabilistic Distributed Algorithms
  AVACS Technical Report, Band: 57, 2010
• Ralf Wimmer, Bernd Becker
  Correctness Issues of Symbolic Bisimulation Computation for Markov Chains
  2010 Int'l GI/ITG Conference on “Measurement, Modelling and Evaluation of Computing Systems”, Springer-Verlag, Band: 5987, Seiten: 287 - 301
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Bisimulation reduction is a classical means tofight the infamous state space explosion problem, which limits theapplicability of automated methods for verification like modelchecking. A signature-based method, originally developed by Blom andOrzan for labeled transition systems and adapted for Markov chains byDerisavi, has proved to be very efficient. It is possible to implement itsymbolically using binary decision diagrams such that it is able tohandle very large state spaces efficiently. We will show, however,that for Markov chains this algorithm suffers from numericalinstabilities, which often result in too large quotient systems. Wewill present and experimentally evaluate two different approaches toavoid these problems: first the usage of rational arithmetic, andsecond an approach not only to represent the system structure but alsothe transition rates symbolically. In addition, this allows us tomodify their actual values after the quotient computation.
• Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
  DTMC Model Checking by SCC Reduction
  2010 Int'l Conf. on Quantitative Evaluation of Systems, IEEE Computer Society, Seiten: 37 - 46
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Discrete-Time Markov Chains (DTMCs) are a widely-usedformalism to model probabilistic systems. On the one hand, availabletools like \textsc{Prism} or \textsc{Mrmc} offer efficient \emph{modelchecking} algorithms and thus support the verification of DTMCs.However, these algorithms do not provide any diagnostic informationin the form of \emph{counterexamples}, which arehighly important for the correction of erroneous systems. On the otherhand, there exist several approaches to generate counterexamples forDTMCs, but all these approaches require the model checking result forcompleteness.In this paper we introduce a model checking algorithm for DTMCs thatalso supports the generation of counterexamples. Our algorithm,based on the detection and abstraction of strongly connectedcomponents, offers \emph{abstract} counterexamples, which can beinteractively refined by the user.
• Natalia Kalinnik, Erika Ábrahám, Tobias Schubert, Ralf Wimmer, Bernd Becker
  Exploiting Different Strategies for the Parallelization of an SMT Solver
  2010 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Fraunhofer Verlag, Seiten: 97 - 106
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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 isexplored in parallel by several copies of the same solver but usingdifferent heuristics to guide the search. We also combine bothapproaches such that solvers examine disjoint parts of the searchspace using different heuristics. The main contribution of the paper is to study the performances of different techniques for parallelizing iSAT.
• Ralf Wimmer, Bettina Braitling, Bernd Becker, Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns, Abhishek Dhama, Oliver Theel
  Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems
  2010 Int'l Conf. on Quantitative Evaluation of Systems, IEEE Computer Society, Seiten: 27 - 36
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Model checkers for concurrent probabilistic systems havebecome very popular within the last decade. The study of long-runaverage behavior has however received only scant attention in thisarea, at least from the implementation perspective. This paperstudies the problem of how to efficiently realize an algorithm forcomputing optimal long-run average reward values for concurrentprobabilistic systems. At its core is a variation of Howard andVeinott's algorithm for Markov decision processes, where symbolicand non-symbolic representations are intertwined in an effectivemanner: the state space is represented using binary decisiondiagrams, while the linear equation systems which have to be solvedfor the induced Markov chains to improve the current scheduler aresolved using an explicit state representation. In order to keep thelatter small, we apply a symbolic bisimulation minimizationalgorithm 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, andsometimes uses considerably less memory than a fully explicitimplementation.
• Ralf Wimmer, Salem Derisavi, Holger Hermanns
  Symbolic Partition Refinement with Automatic Balancing of Time and Space
  2010 Performance Evaluation, Band: 67, Nummer: 9, Seiten: 815 - 835
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2009

 nach oben zur Jahresübersicht

• Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, Bernd Becker
  Picoso - A Parallel Interval Constraint Solver
  2009 Int'l Conf. on Parallel and Distributed Processing Techniques and Applications, CSREA Press, Seiten: 473 - 479
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  This paper describes the parallel interval constraint solver 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.
• Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Jan Rakow, Ralf Wimmer, Bernd Becker
  Compositional Dependability Evaluation for Statemate
  2009 IEEE Trans. on Software Engineering, Band: 35, Nummer: 2, Seiten: 274 - 292
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  Software and system dependability is getting ever more important inembedded system design. Current industrial practice of model-basedanalysis is supported by state-transition diagrammatic notationssuch as Statecharts. State-of-the-art modelling tools like\textsc{Statemate} support safety and failure-effect analysis atdesign time, but restricted to qualitative properties. This paperreports on a (plug-in) extension of \textsc{Statemate} enabling theevaluation of quantitative dependability properties at design time.The extension is compositional in the way the model is augmentedwith probabilistic timing information. This fact is exploited in theconstruction of the underlying mathematical model, a uniformcontinuous-time Markov decision process, on which we are able tocheck requirements of the form: \emph{``The probability to hit asafety-critical system configuration within a mission time of 3hours is at most 0.01.''} We give a detailed explanation of theconstruction and evaluation steps making this possible, and reporton a nontrivial case study of a high-speed train signalling systemwhere the tool has been applied successfully.
• Ralf Wimmer, Bettina Braitling, Bernd Becker
  Counterexample Generation for Discrete-time Markov Chains using Bounded Model Checking
  2009 Int'l Conf. on Verification, Model Checking and Abstract Interpretation, Springer-Verlag, Band: 5403, Seiten: 366 - 380
• Abhis, hek Dhama, Oliver Theel, Pepijn Crouzen, Holger Hermanns, Ralf Wimmer, Bernd Becker
  Dependability Engineering of Silent Self-Stabilizing Systems
  2009 Int'l Symp. on Stabilization, Safety, and Security of Distributed Systems, Springer-Verlag, Band: 5873, Seiten: 238 - 253
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  s 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.

2008

 nach oben zur Jahresübersicht

• Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd Becker
  Probabilistic Model Checking and Reliability of Results
  2008 IEEE Design and Diagnostics of Electronic Circuits and Systems, IEEE Computer Science Press, Seiten: 207 - 212
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.\par 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, Marc Herbstritt, Natalia Kalinnik, Matthew Lewis, Juri Lichtner, Tobias Nopper, Ralf Wimmer
  Propositional Approximations for Bounded Model Checking of Partial Circuit Designs
  2008 IEEE Int'l Conf. on Computer Design, IEEE Computer Society Press, Seiten: 52 - 59
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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, Salem Derisavi, Holger Hermanns
  Symbolic Partition Refinement with Dynamic Balancing of Time and Space
  2008 Int'l Conf. on Quantitative Evaluation of Systems, IEEE Computer Science Press, Seiten: 65 - 74
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• Ralf Wimmer, Alexander Kortus, Marc Herbstritt, Bernd Becker
  The Demand for Reliability in Probabilistic Verification
  2008 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 99 - 108
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.\par 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.

2007

 nach oben zur Jahresübersicht

• Ralf Wimmer, Marc Herbstritt, Bernd Becker
  Forwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation
  2007 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 203 - 212
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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) \emph{block forwarding} updates in-situ newly refined blocks of the partition, (2) \emph{split-driven refinement} approximates the blocks that may be refined, and (3) \emph{block ordering} heuristically suggests a good order in which the blocks will be refined.\par 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, Marc Herbstritt, Bernd Becker
  Optimization Techniques for BDD-based Bisimulation Minimization
  2007 Great Lakes Symp. on VLSI, ACM Press, Seiten: 405 - 410
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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, Alexander Kortus, Marc Herbstritt, Bernd Becker
  Symbolic Model Checking for DTMCs with Exact and Inexact Arithmetic
  AVACS Technical Report, Nummer: 30, 2007
• Ralf Wimmer, Holger Hermanns, Marc Herbstritt, Bernd Becker
  Towards Symbolic Stochastic Aggregation
  AVACS Technical Report, Nummer: 16, 2007

2006

 nach oben zur Jahresübersicht

• Ralf Wimmer, Tobias Nopper, Marc Herbstritt, Christoph Löffler, Bernd Becker
  Collaborative Exercise Management
  2006 World Conf. on E-Learning in Corporate, Government, Healthcare, and Higher Education, Association for the Advancement of Computing in Education (AACE), Seiten: 3127 - 3134
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.
• 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
  AVACS Technical Report, Band: 8, 2006
• Eckard Böde, Marc Herbstritt, Holger Hermanns, Sven Johr, Thomas Peikenkamp, Reza Pulungan, Ralf Wimmer, Bernd Becker
  Compositional Performability Evaluation for STATEMATE
  2006 Int'l Conf. on Quantitative Evaluation of Systems, IEEE Computer Society, Seiten: 167 - 178
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  le 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.
• Ralf Wimmer, Marc Herbstritt, Bernd Becker
  Minimization of Large State Spaces using Symbolic Branching Bisimulation
  2006 IEEE Design and Diagnostics of Electronic Circuits and Systems, IEEE Computer Society Press, Seiten: 9 - 14
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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, Marc Herbstritt, Holger Hermanns, Kelley Strampp, Bernd Becker
  Sigref - A Symbolic Bisimulation Tool Box
  2006 Int'l Symp. on Automated Technology for Verification and Analysis, Springer-Verlag, Band: 4218, Seiten: 477 - 492
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.

2005

 nach oben zur Jahresübersicht

• Bernd Becker, Markus Behle, Friedrich Eisenbrand, Ralf Wimmer
  Cut Framework
  2005 Int'l Workshop on Efficient and Experimental Algorithms, Springer Verlag, Band: 3503, Seiten: 452 - 463
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.\par 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.\par 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

 nach oben zur Jahresübersicht

• Bernd Becker, Markus Behle, Friedrich Eisenbrand, Martin Fränzle, 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
  2004 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Shaker Verlag, Seiten: 65 - 75
  » Kurzfassung anzeigen« Kurzfassung verbergen
  Kurzfassung

  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.