59 citations · 458 across the 94 of their papers we have counts for
9 papers · 1 filter
Probabilistic Model Checking for Complex Cognitive Tasks -- A case study in human-robot interaction
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen +1
This paper proposes to use probabilistic model checking to synthesize optimal robot policies in multi-tasking autonomous systems that are subject to human-robot interaction. Given…
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…
Proving Linearizability via Branching Bisimulation
Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin +1
Linearizability and progress properties are key correctness notions for concurrent objects. However, model checking linearizability has suffered from the PSPACE-hardness of the tra…
Inferring Covariances for Probabilistic Programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
We study weakest precondition reasoning about the (co)variance of outcomes and the variance of run-times of probabilistic programs with conditioning. For outcomes, we show that app…
Bounded Model Checking for Probabilistic Programs
Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski +2
In this paper we investigate the applicability of standard model checking approaches to verifying properties in probabilistic programming. As the operational model for a standard p…
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…
Reasoning about Recursive Probabilistic Programs
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen +1
This paper presents a wp-style calculus for obtaining expectations on the outcomes of (mutually) recursive probabilistic programs. We provide several proof rules to derive one-- an…
Parameter Synthesis for Markov Models: Faster Than Ever
Tim Quatmann, Christian Dehnert, Nils Jansen +2
We propose a simple technique for verifying probabilistic models whose transition probabilities are parametric. The key is to replace parametric transitions by nondeterministic cho…
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja +1
This paper presents a wp-style calculus for obtaining bounds on the expected run-time of probabilistic programs. Its application includes determining the (possibly infinite) expect…