2017

 back to the year overview

• 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, volume: 29, issue: 4, pages: 629 - 649
  » show abstract« hide abstract
  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.

2015

 back to the year overview

• 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), volume: 8931, pages: 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, volume: 9409, pages: 19 - 34
  » show abstract« hide abstract
  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.

2014

 back to the year overview

• 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 , volume: EPTCS
  » show abstract« hide abstract
  Abstract

  abstraction.

2013

 back to the year overview

• 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”, pages: 243 - 254
  » show abstract« hide abstract
  Abstract

  cases.

2011

 back to the year overview

• 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, pages: 89 - 97
  » show abstract« hide abstract
  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.
• 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, volume: 6722, pages: 75 - 89
  » show abstract« hide abstract
  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.\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.
• 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, volume: 14, pages: 19 - 28
  » show abstract« hide abstract
  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.

2010

 back to the year overview

• 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, volume: 57, 2010
• 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, pages: 27 - 36
  » show abstract« hide abstract
  Abstract

  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.

2009

 back to the year overview

• Piet Engelke, Bernd Becker, Michel Renovell, Jürgen Schlöffel, Bettina Braitling, Ilia Polian
  SUPERB: Simulator Utilizing Parallel Evaluation of Resistive Bridges
  2009 ACM Trans. on Design Automation of Electronic Systems, volume: 14, issue: 4, pages: 56:1 - 56:21
• 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, volume: 5403, pages: 366 - 380

2007

 back to the year overview

• Piet Engelke, Bettina Braitling, Ilia Polian, Michel Renovell, Bernd Becker
  SUPERB: Simulator Utilizing Parallel Evaluation of Resistive Bridges
  2007 IEEE Asian Test Symp., pages: 433 - 438
  » show abstract« hide abstract
  Abstract

  A high-performance resistive bridging fault simulator SUPERB (Simulator Utilizing Parallel Evaluation of Resistive Bridges) is proposed. It is based on fault sectioning in combination with parallel-pattern or parallel-fault multiple-stuck-at simulation. It outperforms a conventional interval-based resistive bridging fault simulator by 60X to 120X while delivering identical results. Further competing tools are outperformed by several orders of magnitude.