+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Montag, 3. Dezember 2018, 15.00 Uhr Ort: Gebäude E3, Raum 9007, Ahornstr. 55 Referent: Dipl.-Inform. Christian Hensel Thema: The Probabilistic Model Checker Storm -- Symbolic Methods for Probabilistic Model Checking Abstract: In a world in which we increasingly rely on safety critical systems that simultaneously are becoming ever more complex, formal methods provide a means to mathematically rigorously prove systems correct. Model checking is a fully automated technique that is successfully applied in the verification of software and hardware circuits. Probabilistic model checking extends traditional model checking to deal with systems exhibiting stochastic behavior. As model checking can be simplistically viewed as an exhaustive exploration of the state space of the model under consideration, it suffers from the curse of dimensionality: State spaces grow exponentially in the number of components and variables and they quickly become too large to be effectively manageable, a problem that is typically referred to as state space explosion. Symbolic methods have helped to alleviate this problem substantially. Rather than considering states and transitions of the system individually, they instead exploit structure in the model and treat sets of states and transitions simultaneously. Model checkers based on symbolic techniques dominate the landscape of hardware and software model checking. In the probabilistic setting, symbolic methods show potential but are arguably not on par with their qualitative counterparts. In this talk, we summarize our advances in the field of symbolic techniques in the context of probabilistic model checking. After a brief introduction, we show how to reduce probabilistic systems including nondeterministic choices that are represented using decision diagrams with respect to bisimulation minimization, a well-studied technique for factoring out symmetry. Then, we show how to compute and refine bounds on reachability probabilities for infinite-state systems before presenting our novel probabilistic model checker Storm, which encompasses the aforementioned techniques and significantly outperforms competing tools on a set of standard benchmarks. Es laden ein: Die Dozenten der Informatik