Bettina Braitling
Liste filtern : Jahre: 2015 |
2014 |
2013 |
2011 |
2010 |
2009 |
2007 | alle anzeigen nach oben zur Jahresübersicht Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger HermannsAbstraction-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 BeckerCost 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. nach oben zur Jahresübersicht Bettina Braitling, Luis María Ferrer Fioriti, Hassan Hatefi, Ralf Wimmer, Bernd Becker, Holger HermannsMeGARA: 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 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 Markov decision processes. First experiments show that a significant reduction in size is possible using
abstraction. nach oben zur Jahresübersicht Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika ÁbrahámStochastic 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 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. nach oben zur Jahresübersicht Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver Theel, Ralf Wimmer, Bettina Braitling, Bernd BeckerBounded 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ámCounterexample 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. Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika ÁbrahámSMT-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. nach oben zur Jahresübersicht Pepijn Crouzen, Ernst Moritz Hahn, Holger Hermanns, Abhishek Dhama, Oliver Theel, Ralf Wimmer, Bettina Braitling, Bernd BeckerBounded Fairness for Probabilistic Distributed Algorithms AVACS Technical Report , Band : 57, 2010 Ralf Wimmer, Bettina Braitling, Bernd Becker, Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns, Abhishek Dhama, Oliver TheelSymblicit 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. nach oben zur Jahresübersicht Piet Engelke, Bernd Becker, Michel Renovell, Jürgen Schlöffel, Bettina Braitling, Ilia PolianSUPERB: Simulator Utilizing Parallel Evaluation of Resistive Bridges 2009 ACM Trans. on Design Automation of Electronic Systems , Band : 14, Nummer : 4, Seiten : 56:1 - 56:21 Ralf Wimmer, Bettina Braitling, Bernd BeckerCounterexample 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 nach oben zur Jahresübersicht Piet Engelke, Bettina Braitling, Ilia Polian, Michel Renovell, Bernd BeckerSUPERB: Simulator Utilizing Parallel Evaluation of Resistive Bridges 2007 IEEE Asian Test Symp. , Seiten : 433 - 438» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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.