59 citations · 458 across the 94 of their papers we have counts for
12 papers · 1 filter
Scenario-Based Verification of Uncertain MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges +2
We consider Markov decision processes (MDPs) in which the transition probabilities and rewards belong to an uncertainty set parametrized by a collection of random variables. The pr…
Simple Strategies in Multi-Objective MDPs (Technical Report)
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann +1
We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obta…
Are Parametric Markov Chains Monotonic?
Jip Spel, Sebastian Junges, Joost-Pieter Katoen
This paper presents a simple algorithm to check whether reachability probabilities in parametric Markov chains are monotonic in (some of) the parameters. The idea is to construct -…
Multiple Analyses, Requirements Once: simplifying testing & verification in automotive model-based development
Philipp Berger, Johanna Nellen, Joost-Pieter Katoen +3
In industrial model-based development (MBD) frameworks, requirements are typically specified informally using textual descriptions. To enable the application of formal methods, the…
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…
On the Complexity of Reachability in Parametric Markov Decision Processes
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez +1
This paper studies parametric Markov decision processes (pMDPs), an extension to Markov decision processes (MDPs) where transitions probabilities are described by polynomials over…
Aiming Low Is Harder -- Induction for Lower Bounds in Probabilistic Program Verification
Marcel Hark, Benjamin Lucien Kaminski, Jürgen Giesl +1
We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our…
Shepherding Hordes of Markov Chains
Milan Ceska, Nils Jansen, Sebastian Junges +1
This paper considers large families of Markov chains (MCs) that are defined over a set of parameters with finite discrete domains. Such families occur in software product lines, pl…
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…
Alternating Weak Automata from Universal Trees
Laure Daviaud, Marcin Jurdziński, Karoliina Lehtinen
An improved translation from alternating parity automata on infinite words to alternating weak automata is given. The blow-up of the number of states is related to the size of the…
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…
A Pre-Expectation Calculus for Probabilistic Sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu +3
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone func…