59 citations · 111 across the 11 of their papers we have counts for
12 papers
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…
Sampling-Based Verification of CTMCs with Uncertain Rates
Thom S. Badings, Nils Jansen, Sebastian Junges +2
We employ uncertain parametric CTMCs with parametric transition rates and a prior on the parameter values. The prior encodes uncertainty about the actual transition rates, while th…
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…
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…
Parameter Synthesis for Markov Models: Covering the Parameter Space
Sebastian Junges, Erika Ábrahám, Christian Hensel +4
Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such a…
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…
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…
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…