arXiv subjects

Sascha Klüppelholz

Publications and source records attributed to Sascha Klüppelholz.

14 recordsLinked to original sources

arXiv2026

Towards Actionable Strategy Certificates in Stochastic Parity Games

We propose a new approach for synthesizing large sets of winning strategies in stochastic parity games (2.5-player games) with quantitative objectives. Instead of computing a single, fully specified winning strategy, we introduce Actionable Strategy Certificates (ASCerts) as a local and permissive representation of a large class of system player winning strategies. To this end, we extend known certificates for stochastic invariants to the setting of games. Our certificates prove that synthesized strategies remain within a safe region of the game with probability at least $λ\in [0,1]$. As such, the certificates enhance the trustworthiness of synthesized strategies. The crux of our approach is to reinterpret and leverage the certificates as concise, local, and permissive representation of (possibly infinitely many) strategies. By carefully combining our certificates for stochastic invariants with strategy templates for almost-sure winning, we obtain a novel local representation of quantitatively winning strategies in stochastic parity games. This enables efficient synthesis, adaptation, and runtime strategy extraction, making ASCerts well suited for logical control in uncertain and adversarial environments. We provide a proof-of-concept implementation and demonstrate the potential of applying ASCerts in runtime adaptation in a case study.

cs.GT↗

arXiv2026

Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes $ω$-regular languages by processing their ultimately periodic words. FDFA are known to enjoy many good properties and can be exponentially more succinct than deterministic $ω$-automata with Rabin, Streett or parity acceptance. This paper addresses two main questions: (1) Are FDFA suitable for probabilistic model checking purposes? and (2) Is it possible to obtain an even more compact representation of $ω$-regular languages by allowing the components of an FDFA to be unambiguous instead of deterministic? Question (1) is answered in the affirmative by presenting the first polynomial-time algorithm for computing the probability that a discrete-time Markov chain satisfies an $ω$-regular property represented as an FDFA. Question (2) is motivated by the fact that unambiguous finite automata may require exponentially fewer states than deterministic ones. This paper introduces a model of families of unambiguous finite automata (FUFA) that captures the class of $ω$-regular languages. FUFA can be exponentially more succinct than both FDFA and unambiguous Büchi automata, and there is a single-exponential translation from linear temporal logic (LTL) to FUFA. This stands in contrast to a double-exponential lower bound for the translation from LTL to FDFA. Moreover, the polynomial-time probabilistic model checking algorithm for discrete-time Markov chains against FDFA-specifications is extended to the case where the property is represented by an FUFA with a deterministic leading automaton.

cs.FL↗

arXiv2026

Backward Responsibility in Transition Systems Beyond Safety

As the complexity of software systems rises, methods for explaining their behaviour are becoming ever-more important. When a system fails, it is critical to determine which of its components are responsible for this failure. Within the verification community, one approach uses graph games and Shapley values to ascribe a responsibility value to every state of a transition system. As this is done with respect to a specific failure, it is called backward responsibility. This paper provides tight complexity bounds for the computation of backward responsibility values for reachability, Büchi and parity objectives. For Büchi objectives, a polynomial algorithm is given to determine the set of responsible states, i.e. states with positive responsibility value. To analyse systems that are too large for standard methods, the paper presents a novel refinement algorithm that iteratively finds the set of responsible states. Several heuristics are proposed to guide the refinement algorithm. Its utility is demonstrated with a tool that implements refinement in addition to several other responsibility computation techniques.

cs.FL↗

arXiv2026

Concurrent Permissive Strategy Templates

Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semantics naturally capture the synchronous interactions characteristic of many cyber-physical systems (CPS), their adoption in CPS design remains limited. Building on the concept of permissive strategy templates (PeSTels) for turn-based games, we introduce concurrent (permissive) strategy templates (ConSTels) -- a novel representation for sets of randomized winning strategies in concurrent games with Safety, Büchi, and Co-Büchi objectives. ConSTels compactly encode infinite families of strategies, thereby supporting both offline and online adaptation. Offline, we exploit compositionality to enable incremental synthesis: combining ConSTels for simpler objectives into non-conflicting templates for more complex combined objectives. Online, we demonstrate how ConSTels facilitate runtime adaptation, adjusting action probabilities in response to observed opponent behavior to optimize performance while preserving correctness. We implemented ConSTel synthesis and adaptation in a prototype tool and experimentally show its potential.

cs.GT↗

arXiv2025

Certificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes

Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustworthiness and explainability of model checking tools, we present independently checkable certificates and witnesses for multi-objective ω-regular queries in Markov decision processes. For the certification, we extend and improve existing certificates for the decomposition of maximal end components and reachability properties. We then derive mixed-integer linear programs (MILPs) for finding minimal witnessing subsystems. For the special case of Markov chains and LTL properties, we use unambiguous Büchi automata to find witnesses, resulting in an algorithm that requires single-exponential space. Existing approaches based on deterministic automata require doubly-exponential space in the worst case. Finally, we consider the practical computation of our certificates and witnesses and provide an implementation of the developed techniques, along with an experimental evaluation, demonstrating the efficacy of our techniques.

cs.LO↗

arXiv2025

Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains

We introduce $(\varepsilon, δ)$-bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsilon, δ)$-bisimulation allows the use of different tolerances for the transition probabilities ($\varepsilon$, additive) and total exit rates ($δ$, multiplicative) of states. Fundamental properties of the notion, as well as bounds on the absolute difference of time- and reward-bounded reachability probabilities for $(\varepsilon,δ)$-bisimilar states, are established.

cs.LO↗

arXiv2025

Certificates and Witnesses for Multi-Objective Queries in Markov Decision Processes

Certifying verification algorithms not only return whether a given property holds or not, but also provide an accompanying independently checkable certificate and a corresponding witness. The certificate can be used to easily validate the correctness of the result and the witness provides useful diagnostic information, e.g. for debugging purposes. Thus, certificates and witnesses substantially increase the trustworthiness and understandability of the verification process. In this work, we consider certificates and witnesses for multi-objective reachability-invariant and mean-payoff queries in Markov decision processes, that is conjunctions or disjunctions either of reachability and invariant or mean-payoff predicates, both universally and existentially quantified. Thereby, we generalize previous works on certificates and witnesses for single reachability and invariant constraints. To this end, we turn known linear programming techniques into certifying algorithms and show that witnesses in the form of schedulers and subsystems can be obtained. As a proof-of-concept, we report on implementations of certifying verification algorithms and experimental results.

cs.LO↗

arXiv2024

Formal Quality Measures for Predictors in Markov Decision Processes

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 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.

cs.LO↗

arXiv2024

Responsibility in Actor-Based Systems

The enormous growth of the complexity of modern computer systems leads to an increasing demand for techniques that support the comprehensibility of systems. This has motivated the very active research field of formal methods that enhance the understanding of why systems behave the way they do. One important line of research within the verification community relies on formal notions that measure the degree of responsibility of different actors. In this paper, we first provide a uniform presentation of recent work on responsibility notions based on Shapley values for reactive systems modeled by transition systems and considering safety properties. The paper then discusses how to use these formal responsibility notions and corresponding algorithms for three different types of actor sets: the module-based notion serves to reason about the impact of system components on the satisfaction or violation of a safety property. Responsibility values for value-based actor sets and action-based actors allow for the identification of program instructions and control points that have the most influence on a specification violation. Beyond the theoretical considerations, this paper reports on experimental results that provide initial insights into applicability and scalability.

cs.FL↗

arXiv2024

Backward Responsibility in Transition Systems Using General Power Indices

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.

cs.FL↗

arXiv2023

Maximizing the Conditional Expected Reward for Reaching the Goal

The paper addresses the problem of computing maximal conditional expected accumulated rewards until reaching a target state (briefly called maximal conditional expectations) in finite-state Markov decision processes where the condition is given as a reachability constraint. Conditional expectations of this type can, e.g., stand for the maximal expected termination time of probabilistic programs with non-determinism, under the condition that the program eventually terminates, or for the worst-case expected penalty to be paid, assuming that at least three deadlines are missed. The main results of the paper are (i) a polynomial-time algorithm to check the finiteness of maximal conditional expectations, (ii) PSPACE-completeness for the threshold problem in acyclic Markov decision processes where the task is to check whether the maximal conditional expectation exceeds a given threshold, (iii) a pseudo-polynomial-time algorithm for the threshold problem in the general (cyclic) case, and (iv) an exponential-time algorithm for computing the maximal conditional expectation and an optimal scheduler.

cs.LO↗

arXiv2021

Determinization and Limit-determinization of Emerson-Lei automata

We study the problem of determinizing $ω$-automata whose acceptance condition is defined on the transitions using Boolean formulas, also known as transition-based Emerson-Lei automata (TELA). The standard approach to determinize TELA first constructs an equivalent generalized Büchi automaton (GBA), which is later determinized. We introduce three new ways of translating TELA to GBA. Furthermore, we give a new determinization construction which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. We also study limit-determinization of TELA and show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.

cs.FL↗

arXiv2013

Probabilistic Model Checking for Energy Analysis in Software Product Lines

In a software product line (SPL), a collection of software products is defined by their commonalities in terms of features rather than explicitly specifying all products one-by-one. Several verification techniques were adapted to establish temporal properties of SPLs. Symbolic and family-based model checking have been proven to be successful for tackling the combinatorial blow-up arising when reasoning about several feature combinations. However, most formal verification approaches for SPLs presented in the literature focus on the static SPLs, where the features of a product are fixed and cannot be changed during runtime. This is in contrast to dynamic SPLs, allowing to adapt feature combinations of a product dynamically after deployment. The main contribution of the paper is a compositional modeling framework for dynamic SPLs, which supports probabilistic and nondeterministic choices and allows for quantitative analysis. We specify the feature changes during runtime within an automata-based coordination component, enabling to reason over strategies how to trigger dynamic feature changes for optimizing various quantitative objectives, e.g., energy or monetary costs and reliability. For our framework there is a natural and conceptually simple translation into the input language of the prominent probabilistic model checker PRISM. This facilitates the application of PRISM's powerful symbolic engine to the operational behavior of dynamic SPLs and their family-based analysis against various quantitative queries. We demonstrate feasibility of our approach by a case study issuing an energy-aware bonding network device.

cs.SE↗

arXiv2012

Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code

Reliability in terms of functional properties from the safety-liveness spectrum is an indispensable requirement of low-level operating-system (OS) code. However, with evermore complex and thus less predictable hardware, quantitative and probabilistic guarantees become more and more important. Probabilistic model checking is one technique to automatically obtain these guarantees. First experiences with the automated quantitative analysis of low-level operating-system code confirm the expectation that the naive probabilistic model checking approach rapidly reaches its limits when increasing the numbers of processes. This paper reports on our work-in-progress to tackle the state explosion problem for low-level OS-code caused by the exponential blow-up of the model size when the number of processes grows. We studied the symmetry reduction approach and carried out our experiments with a simple test-and-test-and-set lock case study as a representative example for a wide range of protocols with natural inter-process dependencies and long-run properties. We quickly see a state-space explosion for scenarios where inter-process dependencies are insignificant. However, once inter-process dependencies dominate the picture models with hundred and more processes can be constructed and analysed.

cs.LO↗