Author name cluster

Jakob Piribauer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

10 papers

2 author rows

AAAI Conference 2026 Conference Paper

Temporal Properties of Conditional Independence in Dynamic Bayesian Networks

Rajab Aghamov
Christel Baier
Joël Ouaknine
Jakob Piribauer
Mihir Vahanwala
Isa Vialard

Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over time. In this paper, we study the verification of the evolution of conditional-independence (CI) propositions against temporal logic specifications. To this end, we consider two specification formalisms over CI propositions: linear temporal logic (LTL), and non-deterministic Büchi automata (NBAs). This problem has two variants. Stochastic CI properties take the given concrete probability distributions into account, while structural CI properties are viewed purely in terms of the graphical structure of the DBN. We show that deciding whether a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, which is a long-standing open problem in number theory. On the other hand, we show that verifying the evolution of structural CI propositions against LTL and NBA specifications is in PSPACE, and is hard for both NP and coNP. We also identify natural restrictions on the graphical structure of the DBN that make the verification of structural CI properties tractable.

PDF Details DOI

AAAI Conference 2025 Conference Paper

Formal Quality Measures for Predictors in Markov Decision Processes

Christel Baier
Sascha Klüppelholz
Jakob Piribauer
Robin Ziemek

In adaptive systems, predictors are used to anticipate changes in the system’s state or behavior that may require system adaption, e.g., changing its configuration or adjusting resource allocation. Therefore, the quality of predictors is crucial for the overall reliability and performance of the system under control. This paper studies predictors in systems exhibiting probabilistic and non-deterministic behavior modelled as Markov decision processes (MDPs). Main contributions are the introduction of quantitative notions that measure the effectiveness of predictors in terms of their average capability to predict the occurrence of failures or other undesired system behaviors. The average is taken over all memoryless policies. We study two classes of such notions. One class is inspired by concepts that have been introduced in statistical analysis to explain the impact of features on the decisions of binary classifiers (such as precision, recall, f-score). Second, we study a measure that borrows ideas from recent work on probability-raising causality in MDPs and determines the quality of a predictor by the fraction of memoryless policies under which (the set of states in) the predictor is a probability-raising cause for the considered failure scenario.

PDF Details DOI

KR Conference 2025 Conference Paper

Model Checking Linear Temporal Logic with Standpoint Modalities

Rajab Aghamov
Christel Baier
Toghrul Karimov
Rupak Majumdar
Joël Ouaknine
Jakob Piribauer
Timm Spork

Standpoint linear temporal logic (SLTL) is a recently introduced extension of classical linear temporal logic (LTL) with standpoint modalities. Intuitively, these modalities allow to express that, from agent a's standpoint, it is conceivable that a given formula holds. Besides the standard interpretation of the standpoint modalities we introduce four new semantics, which differ in the information an agent can extract from the history. We provide a general model checking algorithm applicable to SLTL under any of the five semantics. Furthermore we analyze the computational complexity of the corresponding model checking problems, obtaining PSPACE-completeness in three cases, which stands in contrast to the known EXPSPACE-completeness of the SLTL satisfiability problem.

PDF Details DOI

AAAI Conference 2024 Conference Paper

Backward Responsibility in Transition Systems Using General Power Indices

Christel Baier
Roxane van den Bossche
Sascha Klüppelholz
Johannes Lehmann
Jakob Piribauer

To improve reliability and the understanding of AI systems, there is increasing interest in the use of formal methods, e.g. model checking. Model checking tools produce a counterexample when a model does not satisfy a property. Understanding these counterexamples is critical for efficient debugging, as it allows the developer to focus on the parts of the program that caused the issue. To this end, we present a new technique that ascribes a responsibility value to each state in a transition system that does not satisfy a given safety property. The value is higher if the non-deterministic choices in a state have more power to change the outcome, given the behaviour observed in the counterexample. For this, we employ a concept from cooperative game theory – namely general power indices, such as the Shapley value – to compute the responsibility of the states. We present an optimistic and pessimistic version of responsibility that differ in how they treat the states that do not lie on the counterexample. We give a characterisation of optimistic responsibility that leads to an efficient algorithm for it and show computational hardness of the pessimistic version. We also present a tool to compute responsibility and show how a stochastic algorithm can be used to approximate responsibility in larger models. These methods can be deployed in the design phase, at runtime and at inspection time to gain insights on causal relations within the behavior of AI systems.

PDF Details DOI

MFCS Conference 2024 Conference Paper

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 end, the novel notion of demonic variance is introduced: For a random variable X in an MDP ℳ, it is defined as 1/2 times the maximal expected squared distance of the values of X in two independent execution of ℳ in which also the non-deterministic choices are resolved independently by two distinct schedulers. It is shown that the demonic variance is between 1 and 2 times as large as the maximal variance of X in ℳ that can be achieved by a single scheduler. This allows defining a non-determinism score for ℳ and X measuring how strongly the difference of X in two executions of ℳ can be influenced by the non-deterministic choices. Properties of MDPs ℳ with extremal values of the non-determinism score are established. Further, the algorithmic problems of computing the maximal variance and the demonic variance are investigated for two random variables, namely weighted reachability and accumulated rewards. In the process, also the structure of schedulers maximizing the variance and of scheduler pairs realizing the demonic variance is analyzed.

Details

GandALF Workshop 2023 Workshop Paper

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 explain what went wrong on a given counterexample execution that shows that a system does not satisfy a given specification. To this end, this paper investigates a notion of counterfactual causality in transition systems based on Stalnaker's and Lewis' semantics of counterfactuals in terms of most similar possible worlds and introduces a novel corresponding notion of counterfactual causality in two-player games. Using distance functions between paths in transition systems, this notion defines whether reaching a certain set of states is a cause for the violation of a reachability or safety property. Similarly, using distance functions between memoryless strategies in reachability and safety games, it is defined whether reaching a set of states is a cause for the fact that a given strategy for the player under investigation is losing. The contribution of the paper is two-fold: In transition systems, it is shown that counterfactual causality can be checked in polynomial time for three prominent distance functions between paths. In two-player games, the introduced notion of counterfactual causality is shown to be checkable in polynomial time for two natural distance functions between memoryless strategies. Further, a notion of explanation that can be extracted from a counterfactual cause and that pinpoints changes to be made to the given strategy in order to transform it into a winning strategy is defined. For the two distance functions under consideration, the problem to decide whether such an explanation imposes only minimal necessary changes to the given strategy with respect to the used distance function turns out to be coNP-complete and not to be solvable in polynomial time if P is not equal to NP, respectively.

PDF Details DOI

MFCS Conference 2023 Conference Paper

Entropic Risk for Turn-Based Stochastic Games

Christel Baier
Krishnendu Chatterjee
Tobias Meggendorfer
Jakob Piribauer

Entropic risk (ERisk) is an established risk measure in finance, quantifying risk by an exponential re-weighting of rewards. We study ERisk for the first time in the context of turn-based stochastic games with the total reward objective. This gives rise to an objective function that demands the control of systems in a risk-averse manner. We show that the resulting games are determined and, in particular, admit optimal memoryless deterministic strategies. This contrasts risk measures that previously have been considered in the special case of Markov decision processes and that require randomization and/or memory. We provide several results on the decidability and the computational complexity of the threshold problem, i. e. whether the optimal value of ERisk exceeds a given threshold. In the most general case, the problem is decidable subject to Shanuel’s conjecture. If all inputs are rational, the resulting threshold problem can be solved using algebraic numbers, leading to decidability via a polynomial-time reduction to the existential theory of the reals. Further restrictions on the encoding of the input allow the solution of the threshold problem in NP∩coNP. Finally, an approximation algorithm for the optimal value of ERisk is provided.

Details

Highlights Conference 2022 Conference Abstract

Tradeoffs Between Expectation and Variance in Weighted Markov Decision Processes

Jakob Piribauer

Many verification problems for probabilistic systems address optimal expected values of incurred costs or received rewards. In Markov decision processes (MDPs), a standard operational model combining non-deterministic and probabilistic transitions, these verification questions frequently result in stochastic shortest path problems where the task is to find a scheduler that optimizes the expected value of the amount of weight accumulated before reaching a target state. Other aspects besides the expectation of the resulting probability distribution of the accumulated weights are completely disregarded. In many application areas, however, the uncertainty coming with the probabilistic behavior cannot be neglected. In traffic control systems or energy grids, for example, large variability in the throughput comes at a high cost due to the risk of traffic jams or the difficulty of storing surplus energy. Also a probabilistic program employed in a complex environment might be of more use with a higher expected termination time in exchange for a lower chance of extreme termination times. A standard measure to quantify probabilistic uncertainty is the variance. This talk will address problems arising in finding a good tradeoff between variance and expectation in the stochastic shortest path problem. One way to achieve different tradeoffs is to consider variance-penalized expectations where a multiple of the variance is incurred as a penalty on the obtained expectation. Varying the penalty factor leads to different tradeoffs. We show that variance-penalized expectations in MDPs with non-negative weights can be computed in exponential space and that the corresponding threshold problem whether the optimum exceeds a given rational is in NEXPTIME and EXPTIME-hard. In addition, optimal schedulers can be chosen to be deterministic finite-memory schedulers. Furthermore, the talk will indicate difficulties arising in the question whether there is a scheduler that achieves at least an expectation of e while having variance at most v for given rationals e and v: Schedulers using memory and randomization are necessary here in general. In addition, when plotting possible combinations of expectation and variance that can be achieved by schedulers in an MDP, the resulting feasible region is not convex and the border is composed of parabolic line segments. This indicates a significant contrast to many other problems on weighted MDPs. The talk is based on ongoing joint work with Ocan Sankur and Christel Baier.

Details

Highlights Conference 2021 Conference Abstract

Positivity-hardness results for Markov decision processes

Jakob Piribauer

In this talk, I give a brief overview of a series of novel reductions from the Positivity problem for linear recurrence sequences to various decision problems on Markov decision processes (MDPs). The Positivity problem is a famous number-theoretic problem whose decidability status has been open for many decades. A proof that a problem is Positivity-hard, i. e. at least as hard as the Positivity problem, establishes that the problem exhibits the same inherent mathematical difficulty as the Positivity problem and that it can most likely not be solved with known techniques. The reductions I present are obtained by constructing MDP-gadgets that encode linear recurrence sequences. These gadgets can easily be adjusted depending on the problem on MDPs under consideration. This flexible proof technique is then applied to establish Positivity-hardness of weight-bounded reachability problems, of termination problems for one-counter MDPs, of problems concerning the satisfaction probability of energy objectives, of variants of the stochastic shortest path problem, and of the model-checking problem of frequency-LTL among others. The results of this talk have partly been published in joint work with Christel Baier at ICALP 2020 and are presented in my recently submitted PhD thesis.

Details

GandALF Workshop 2021 Workshop Paper

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. Computing minimal witnessing subsystems is NP-hard already for acyclic Markov chains, but can be done in polynomial time for Markov chains whose underlying graph is a tree. This paper considers the problem for probabilistic systems that are similar to trees or paths. It introduces the parameters directed tree-partition width (dtpw) and directed path-partition width (dppw) and shows that computing minimal witnesses remains NP-hard for Markov chains with bounded dppw (and hence also for Markov chains with bounded dtpw). By observing that graphs of bounded dtpw have bounded width with respect to all known tree similarity measures for directed graphs, the hardness result carries over to these other tree similarity measures. Technically, the reduction proceeds via the conceptually simpler matrix-pair chain problem, which is introduced and shown to be NP-complete for nonnegative matrices of fixed dimension. Furthermore, an algorithm which aims to utilise a given directed tree partition of the system to compute a minimal witnessing subsystem is described. It enumerates partial subsystems for the blocks of the partition along the tree order, and keeps only necessary ones. A preliminary experimental analysis shows that it outperforms other approaches on certain benchmarks which have directed tree partitions of small width.

PDF Details DOI