4 citations · 11 across the 20 of their papers we have counts for
21 papers · 1 filter
On Modal Logics of Full Products of Neighborhood Frames
Rajab Aghamov, Andrey Kudinov, Maik Thanh Nguyen +1
On the product of two neighborhood frames, three natural neighborhood functions can be defined: the horizontal one assigning to a point (x, y) the set of all supersets of the Carte…
The Modal Logic of Abstraction Refinement
Jakob Piribauer, Vinzent Zschuppe
Iterative abstraction refinement techniques are one of the most prominent paradigms for the analysis and verification of systems with large or infinite state spaces. This paper inv…
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Timm Spork, Christel Baier, Joost-Pieter Katoen +2
We introduce -bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsilo…
Multiplicative Rewards in Markovian Models
Christel Baier, Krishnendu Chatterjee, Tobias Meggendorfer +1
This paper studies the expected value of multiplicative rewards, where rewards obtained in each step are multiplied (instead of the usual addition), in Markov chains (MCs) and Mark…
Model Checking Linear Temporal Logic with Standpoint Modalities
Rajab Aghamov, Christel Baier, Toghrul Karimov +4
Standpoint linear temporal logic () is a recently introduced extension of classical linear temporal logic () with standpoint modalities. Intuitively, these modalities al…
Formal Quality Measures for Predictors in Markov Decision Processes
Christel Baier, Sascha Klüppelholz, Jakob Piribauer +1
In adaptive systems, predictors are used to anticipate changes in the systems state or behavior that may require system adaption, e.g., changing its configuration or adjusting reso…
A Spectrum of Approximate Probabilistic Bisimulations
Timm Spork, Christel Baier, Joost-Pieter Katoen +2
This paper studies various notions of approximate probabilistic bisimulation on labeled Markov chains (LMCs). We introduce approximate versions of weak and branching bisimulation,…
Risk-averse optimization of total rewards in Markovian models using deviation measures
Christel Baier, Jakob Piribauer, Maximilian Starke
This paper addresses objectives tailored to the risk-averse optimization of accumulated rewards in Markov decision processes (MDPs). The studied objectives require maximizing the e…
Demonic variance and a non-determinism score for Markov decision processes
Jakob Piribauer
This paper studies the influence of probabilism and non-determinism on some quantitative aspect X of the execution of a system modeled as a Markov decision process (MDP). To this e…
Model Checking Markov Chains as Distribution Transformers
Rajab Aghamov, Christel Baier, Toghrul Karimov +4
The conventional perspective on Markov chains considers decision problems concerning the probabilities of temporal properties being satisfied by traces of visited states. However,…
Counterfactual Causality for Reachability and Safety based on Distance Functions
Julie Parreaux, Jakob Piribauer, Christel Baier
Investigations of causality in operational systems aim at providing human-understandable explanations of why a system behaves as it does. There is, in particular, a demand to expla…
Counterfactual Causality for Reachability and Safety based on Distance Functions
Julie Parreaux, Jakob Piribauer, Christel Baier
Investigations of causality in operational systems aim at providing human-understandable explanations of why a system behaves as it does. There is, in particular, a demand to expla…
Positivity-hardness results on Markov decision processes
Jakob Piribauer, Christel Baier
This paper investigates a series of optimization problems for one-counter Markov decision processes (MDPs) and integer-weighted MDPs with finite state space. Specifically, it consi…
Foundations of probability-raising causality in Markov decision processes
Christel Baier, Jakob Piribauer, Robin Ziemek
This work introduces a novel cause-effect relation in Markov decision processes using the probability-raising principle. Initially, sets of states as causes and effects are conside…
On probability-raising causality in Markov decision processes
Christel Baier, Florian Funke, Jakob Piribauer +1
The purpose of this paper is to introduce a notion of causality in Markov decision processes based on the probability-raising principle and to analyze its algorithmic properties. T…
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…
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…
On Skolem-hardness and saturation points in Markov decision processes
Jakob Piribauer, Christel Baier
The Skolem problem and the related Positivity problem for linear recurrence sequences are outstanding number-theoretic problems whose decidability has been open for many decades. I…
Partial and Conditional Expectations in Markov Decision Processes with Integer Weights
Jakob Piribauer, Christel Baier
The paper addresses two variants of the stochastic shortest path problem ('optimize the accumulated weight until reaching a goal state') in Markov decision processes (MDPs) with in…