59 citations · 458 across the 94 of their papers we have counts for
13 papers · 1 filter
Probabilistic Model Checking Taken by Storm
Matthias Volk, Linus Heck, Sebastian Junges +2
This tutorial paper presents a hands-on perspective on probabilistic model checking with the Storm model checker. Storm is a decade-old model checker that excels in performance and…
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen +2
Fault trees are a key model in reliability analysis. Classical static fault trees (SFT) can best be analysed using binary decision diagrams (BDD). State-based techniques are favora…
The Probabilistic Model Checker Storm
Christian Hensel, Sebastian Junges, Joost-Pieter Katoen +2
We present the probabilistic model checker Storm. Storm supports the analysis of discrete- and continuous-time variants of both Markov chains and Markov decision processes. Storm h…
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Milan Češka, Christian Hensel, Sebastian Junges +1
Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring…
Safety Analysis for Vehicle Guidance Systems with Dynamic Fault Trees
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen +2
This paper considers the design-phase safety analysis of vehicle guidance systems. The proposed approach constructs dynamic fault trees (DFTs) to model a variety of safety concepts…
One Net Fits All: A unifying semantics of Dynamic Fault Trees using GSPNs
Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga +1
Dynamic Fault Trees (DFTs) are a prominent model in reliability engineering. They are strictly more expressive than static fault trees, but this comes at a price: their interpretat…
A storm is Coming: A Modern Probabilistic Model Checker
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen +1
We launch the new probabilistic model checker storm. It features the analysis of discrete- and continuous-time variants of both Markov chains and MDPs. It supports the PRISM and JA…
The Probabilistic Model Checker Storm (Extended Abstract)
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen +1
We present a new probabilistic model checker Storm. Using state-of-the-art libraries, we aim for both high performance and versatility. This extended abstract gives a brief overvie…
Advancing Dynamic Fault Tree Analysis
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen
This paper presents a new state space generation approach for dynamic fault trees (DFTs) together with a technique to synthesise failures rates in DFTs. Our state space generation…
Safety-Constrained Reinforcement Learning for MDPs
Sebastian Junges, Nils Jansen, Christian Dehnert +2
We consider controller synthesis for stochastic and partially unknown environments in which safety is essential. Specifically, we abstract the problem as a Markov decision process…
Accelerating Parametric Probabilistic Verification
Nils Jansen, Florian Corzilius, Matthias Volk +4
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…
High-level Counterexamples for Probabilistic Automata
Ralf Wimmer, Nils Jansen, Erika Ábrahám +1
Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic syst…
The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains
Nils Jansen, Erika Ábrahám, Maik Scheffler +5
This report presents the tool COMICS, which performs model checking and generates counterexamples for DTMCs. For an input DTMC, COMICS computes an abstract system that carries the…