4 citations · 14 across the 11 of their papers we have counts for
11 papers · 1 filter
Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes
Christel Baier, Calvin Chau, Volodymyr Drobitko +2
Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustwor…
Witnessing Subsystems for Probabilistic Systems with Low Tree Width
Simon Jantsch, Jakob Piribauer, Christel Baier
A standard way of justifying that a certain probabilistic property holds in a system is to provide a witnessing subsystem (also called critical subsystem) for the property. Computi…
Witnessing subsystems for probabilistic systems with low tree width
Simon Jantsch, Jakob Piribauer, Christel Baier
A standard way of justifying that a certain probabilistic property holds in a system is to provide a witnessing subsystem (also called critical subsystem) for the property. Computi…
Causality-Based Game Solving
Christel Baier, Norine Coenen, Bernd Finkbeiner +3
We present a causality-based algorithm for solving two-player reachability games represented by logical constraints. These games are a useful formalism to model a wide array of pro…
From Verification to Causality-based Explications
Christel Baier, Clemens Dubslaff, Florian Funke +4
In view of the growing complexity of modern software architectures, formal models are increasingly used to understand why a system works the way it does, opposed to simply verifyin…
Probabilistic causes in Markov chains
Christel Baier, Florian Funke, Simon Jantsch +2
The paper studies a probabilistic notion of causes in Markov chains that relies on the counterfactuality principle and the probability-raising property. This notion is motivated by…
The Orbit Problem for Parametric Linear Dynamical Systems
Christel Baier, Florian Funke, Simon Jantsch +7
We study a parametric version of the Kannan-Lipton Orbit Problem for linear dynamical systems. We show decidability in the case of one parameter and Skolem-hardness with two or mor…
Responsibility and verification: Importance value in temporal logics
Corto Mascle, Christel Baier, Florian Funke +2
We aim at measuring the influence of the nondeterministic choices of a part of a system on its ability to satisfy a specification. For this purpose, we apply the concept of Shapley…
SWITSS: Computing Small Witnessing Subsystems
Simon Jantsch, Hans Harder, Florian Funke +1
Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as…
Minimal witnesses for probabilistic timed automata
Simon Jantsch, Florian Funke, Christel Baier
Witnessing subsystems have proven to be a useful concept in the analysis of probabilistic systems, for example as diagnostic information on why a given property holds or as input t…
Farkas certificates and minimal witnesses for probabilistic reachability constraints
Florian Funke, Simon Jantsch, Christel Baier
This paper introduces Farkas certificates for lower and upper bounds on minimal and maximal reachability probabilities in Markov decision processes (MDP), which we derive using an…