activity
20242026
most citedCertificates and Witnesses for Multi-objective ω-regular Queries in Markov Decision Processes

1 citations · 1 across the 15 of their papers we have counts for

collaborators

17 papers

cs.GT2026

Towards Actionable Strategy Certificates in Stochastic Parity Games

Christel Baier, Diane Cauquil, Calvin Chau +2

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 singl…

cs.FL2026

Probabilistic Model Checking via Families of Deterministic and Unambiguous Finite Automata

Christel Baier, Sascha Klüppelholz, Timm Spork

Families of deterministic finite automata (FDFA) have been introduced as a concise automaton model that characterizes -regular languages by processing their ultimately periodic…

cs.GT2026

Concurrent Permissive Strategy Templates

Ashwani Anand, Christel Baier, Calvin Chau +4

Two-player games on finite graphs provide a rigorous foundation for modeling the strategic interaction between reactive systems and their environment. While concurrent game semanti…

cs.AI2025

Temporal Properties of Conditional Independence in Dynamic Bayesian Networks

Rajab Aghamov, Christel Baier, Joel Ouaknine +3

Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over…

cs.LO2025★ 1 cited

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…

cs.FL2025

Backward Responsibility in Transition Systems Beyond Safety

Christel Baier, Rio Klatt, Sascha Klüppelholz +2

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…

cs.LO2025

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…

cs.LO2025

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…

cs.LO2025

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…

cs.LO2024

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…

cs.FL2024

Responsibility in Actor-Based Systems

Christel Baier, Sascha Klüppelholz, Johannes Lehmann

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…

cs.LO2024

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,…

cs.LO2024

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…

cs.LO2024

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,…

cs.LO2024

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

Christel Baier, Calvin Chau, Sascha Klüppelholz

Certifying verification algorithms not only return whether a given property holds or not, but also provide an accompanying independently checkable certificate and a corresponding w…

math.DS2024

Linear dynamical systems with continuous weight functions

Rajab Aghamov, Christel Baier, Toghrul Karimov +2

In discrete-time linear dynamical systems (LDSs), a linear map is repeatedly applied to an initial vector yielding a sequence of vectors called the orbit of the system. A weight fu…

cs.FL2024

Backward Responsibility in Transition Systems Using General Power Indices

Christel Baier, Roxane van den Bossche, Sascha Klüppelholz +2

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 counterex…