Holger Hermanns

AAAI Conference 2026 Conference Paper

Probabilistic Safety Verification of Neural Policies via Predicate Abstraction

• Marcel Vinzent
• Holger Hermanns
• Jörg Hoffmann

Neural networks are increasingly important to learn action policies. Policy predicate abstraction (PPA) verifies safety of such a neural policy pi by over-approximating the state space subgraph induced by pi and using counterexample-guided abstraction refinement (CEGAR) to iteratively refine the abstraction. So far, PPA verifies safety in non-deterministic systems. This work extends PPA to probabilistic verification. Extending the abstract state space computation is relatively straightforward. Abstraction refinement, however, becomes substantially more complex, due to the more intricate form of counterexamples and the various sources of spuriousness it entails. We tackle this challenge by drawing inspiration from prior work on probabilistic CEGAR, empowering it to deal with neural pi. The resulting algorithm decides whether pi is safe with respect to a desired upper bound on unsafety probability. Invoking the algorithm incrementally, we can also derive upper and lower bounds automatically. Our experiments show that these algorithms can derive non-trivial bounds, whereas encodings into state-of-the-art probabilistic model checkers turn out to be ineffective.

AAAI Conference 2026 Conference Paper

SL-CBM: Enhancing Concept Bottleneck Models with Semantic Locality for Better Interpretability

• Hanwei Zhang
• Luo Cheng
• Rui Wen
• Yang Zhang
• Lijun Zhang
• Holger Hermanns

Explainable AI (XAI) is crucial for building transparent and trustworthy machine learning systems, especially in high-stakes domains. Concept Bottleneck Models (CBMs) have emerged as a promising ante-hoc approach that provides interpretable, concept-level explanations by explicitly modeling human-understandable concepts. However, existing CBMs often suffer from poor locality faithfulness, failing to spatially align concepts with meaningful image regions, which limits their interpretability and reliability. In this work, we propose SL-CBM (CBM with Semantic Locality), a novel extension that enforces locality faithfulness by generating spatially coherent saliency maps at both concept and class levels. SL-CBM integrates a 1 × 1 convolutional layer with a cross-attention mechanism to enhance alignment between concepts, image regions, and final predictions. Unlike prior methods, SL-CBM produces faithful saliency maps inherently tied to the model’s internal reasoning, facilitating more effective debugging and intervention. Extensive experiments on image datasets demonstrate that SL-CBM substantially improves locality faithfulness, explanation quality, and intervention efficacy while maintaining competitive classification accuracy. Our ablation studies highlight the importance of contrastive and entropy-based regularization for balancing accuracy, sparsity, and faithfulness. Overall, SL-CBM bridges the gap between concept-based reasoning and spatial explainability, setting a new standard for interpretable and trustworthy concept-based models.

JAIR Journal 2022 Journal Article

Admissibility in Probabilistic Argumentation

• Nikolai Käfer
• Christel Baier
• Martin Diller
• Clemens Dubslaff
• Sarah Alice Gaggl
• Holger Hermanns

Abstract argumentation is a prominent reasoning framework. It comes with a variety of semantics and has lately been enhanced by probabilities to enable a quantitative treatment of argumentation. While admissibility is a fundamental notion for classical reasoning in abstract argumentation frameworks, it has barely been reflected so far in the probabilistic setting. In this paper, we address the quantitative treatment of abstract argumentation based on probabilistic notions of admissibility. Our approach follows the natural idea of defining probabilistic semantics for abstract argumentation by systematically imposing constraints on the joint probability distribution on the sets of arguments, rather than on probabilities of single arguments. As a result, there might be either a uniquely defined distribution satisfying the constraints, but also none, many, or even an infinite number of satisfying distributions are possible. We provide probabilistic semantics corresponding to the classical complete and stable semantics and show how labeling schemes provide a bridge from distributions back to argument labelings. In relation to existing work on probabilistic argumentation, we present a taxonomy of semantic notions. Enabled by the constraint-based approach, standard reasoning problems for probabilistic semantics can be tackled by SMT solvers, as we demonstrate by a proof-of-concept implementation.

KR Conference 2021 Conference Paper

Admissibility in Probabilistic Argumentation

• Christel Baier
• Martin Diller
• Clemens Dubslaff
• Sarah Alice Gaggl
• Holger Hermanns
• Nikolai Käfer

Abstract argumentation is a prominent reasoning framework. It comes with a variety of semantics, and has lately been enhanced by probabilities to enable a quantitative treatment of argumentation. While admissibility is a fundamental notion in the classical setting, it has been merely reflected so far in the probabilistic setting. In this paper, we address the quantitative treatment of argumentation based on probabilistic notions of admissibility in a way that they form fully conservative extensions of classical notions. In particular, our building blocks are not the beliefs regarding single arguments. Instead we start from the fairly natural idea that whatever argumentation semantics is to be considered, semantics systematically induces constraints on the joint probability distribution on the sets of arguments. In some cases there might be many such distributions, even infinitely many ones, in other cases there may be one or none. Standard semantic notions are shown to induce such sets of constraints, and so do their probabilistic extensions. This allows them to be tackled by SMT solvers, as we demonstrate by a proof-of-concept implementation. We present a taxonomy of semantic notions, also in relation to published work, together with a running example illustrating our achievements.

AIJ Journal 2021 Journal Article

What do we want from Explainable Artificial Intelligence (XAI)? – A stakeholder perspective on XAI and a conceptual model guiding interdisciplinary XAI research

• Markus Langer
• Daniel Oster
• Timo Speith
• Holger Hermanns
• Lena Kästner
• Eva Schmidt
• Andreas Sesing
• Kevin Baum

Previous research in Explainable Artificial Intelligence (XAI) suggests that a main aim of explainability approaches is to satisfy specific interests, goals, expectations, needs, and demands regarding artificial systems (we call these “stakeholders' desiderata”) in a variety of contexts. However, the literature on XAI is vast, spreads out across multiple largely disconnected disciplines, and it often remains unclear how explainability approaches are supposed to achieve the goal of satisfying stakeholders' desiderata. This paper discusses the main classes of stakeholders calling for explainability of artificial systems and reviews their desiderata. We provide a model that explicitly spells out the main concepts and relations necessary to consider and investigate when evaluating, adjusting, choosing, and developing explainability approaches that aim to satisfy stakeholders' desiderata. This model can serve researchers from the variety of different disciplines involved in XAI as a common ground. It emphasizes where there is interdisciplinary potential in the evaluation and the development of explainability approaches.

JAIR Journal 2020 Journal Article

Bridging the Gap Between Probabilistic Model Checking and Probabilistic Planning: Survey, Compilations, and Empirical Comparison

• Michaela Klauck
• Marcel Steinmetz
• Jörg Hoffmann
• Holger Hermanns

Markov decision processes are of major interest in the planning community as well as in the model checking community. But in spite of the similarity in the considered formal models, the development of new techniques and methods happened largely independently in both communities. This work is intended as a beginning to unite the two research branches. We consider goal-reachability analysis as a common basis between both communities. The core of this paper is the translation from Jani, an overarching input language for quantitative model checkers, into the probabilistic planning domain definition language (PPDDL), and vice versa from PPDDL into Jani. These translations allow the creation of an overarching benchmark collection, including existing case studies from the model checking community, as well as benchmarks from the international probabilistic planning competitions (IPPC). We use this benchmark set as a basis for an extensive empirical comparison of various approaches from the model checking community, variants of value iteration, and MDP heuristic search algorithms developed by the AI planning community. On a per benchmark domain basis, techniques from one community can achieve state-ofthe-art performance in benchmarks of the other community. Across all benchmark domains of one community, the performance comparison is however in favor of the solvers and algorithms of that particular community. Reasons are the design of the benchmarks, as well as tool-related limitations. Our translation methods and benchmark collection foster crossfertilization between both communities, pointing out specific opportunities for widening the scope of solvers to different kinds of models, as well as for exchanging and adopting algorithms across communities.

AAAI Conference 2020 Conference Paper

Let’s Learn Their Language? A Case for Planning with Automata-Network Languages from Model Checking

• Jorg Hoffmann
• Holger Hermanns
• Michaela Klauck
• Marcel Steinmetz
• Erez Karpas
• Daniele Magazzeni

It is widely known that AI planning and model checking are closely related. Compilations have been devised between various pairs of language fragments. What has barely been voiced yet, though, is the idea to let go of one’s own modeling language, and use one from the other area instead. We advocate that idea here – to use automata-network languages from model checking instead of PDDL – motivated by modeling difficulties relating to planning agents surrounded by exogenous agents in complex environments. One could, of course, address this by designing additional extended planning languages. But one can also leverage decades of work on modeling in the formal methods community, creating potential for deep synergy and integration with their techniques as a side effect. We believe there’s a case to be made for the latter, as one modeling alternative in planning among others.

ICAPS Conference 2018 Conference Paper

Compiling Probabilistic Model Checking into Probabilistic Planning

• Michaela Klauck
• Marcel Steinmetz
• Jörg Hoffmann 0001
• Holger Hermanns

It has previously been observed that the verification of safety properties in deterministic model-checking frameworks can be compiled into classical planning. A similar connection exists between goal probability analysis on either side, yet that connection has not been explored. We fill that gap with a translation from Jani, an input language for quantitative model checkers including the Modest toolset and PRISM, into PPDDL. Our experiments motivate further cross-fertilization between both research areas, specifically the exchange of algorithms. Our study also initiates the creation of new benchmarks for goal probability analysis.

I&C Journal 2018 Journal Article

The quest for minimal quotients for probabilistic and Markov automata

• Christian Eisentraut
• Holger Hermanns
• Johann Schuster
• Andrea Turrini
• Lijun Zhang

One of the prevailing ideas in applied concurrency theory and verification is the concept of automata minimization with respect to strong or weak bisimilarity. The minimal automata can be seen as canonical representations of the behaviour modulo the bisimilarity considered. Together with congruence results wrt. process algebraic operators, this can be exploited to alleviate the notorious state space explosion problem. In this paper, we aim at identifying minimal automata and canonical representations for concurrent probabilistic models. We present minimality and canonicity results for probabilistic and Markov automata modulo strong and weak probabilistic bisimilarity, together with the corresponding minimization algorithms. We also consider weak distribution bisimilarity, originally proposed for Markov automata. For this relation, the quest for minimality does not have a unique answer, since fanout minimality clashes with state and transition minimality. We present an SMT approach to enumerate fanout-minimal models.

LPAR Conference 2018 Conference Paper

Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions

• Holger Hermanns
• Sebastian Biewer
• Pedro R. D'Argenio
• Maximilian A. Köhl

Emission cleaning in modern cars is controlled by embedded software. In this context, the diesel emission scandal has made it apparent that the automotive industry is susceptible to fraudulent behaviour, implemented and effectuated by that control software. Mass effects make the individual controllers altogether have statistically significant adverse effects on people’s health. This paper surveys recent work on the use of rigorous formal techniques to attack this problem. It starts off with an introduction into the dimension and facets of the problem from a software technology perspective. It then details approaches to use (i) model checking for the white-box analysis of the embedded software, (ii) model- based black-box testing to detect fraudulent behaviour under standardized conditions, and (iii) synthesis of runtime monitors for real driving emissions of cars in-the-wild. All these efforts aim at finding ways to eventually ban the problem of doped software, that is, of software that surreptitiously alters its behaviour in certain circumstances – against the interest of the owner or of society.

I&C Journal 2015 Journal Article

Polynomial time decision algorithms for probabilistic automata

• Andrea Turrini
• Holger Hermanns

Deciding in an efficient way weak probabilistic bisimulation in the context of probabilistic automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. This enables us to arrive at a polynomial time algorithm for deciding weak probabilistic bisimulation, and also branching probabilistic bisimulation. We furthermore present several extensions to interesting related problems, in particular weak and branching probabilistic simulation, setting the ground for the development of more effective and compositional analysis algorithms for probabilistic systems.

Highlights Conference 2013 Conference Abstract

Compositional verification and optimization of interactive Markov chains

• Holger Hermanns
• Jan Krčál
• Jan Kretinsky

We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property, an IMC component and a specification of the environment, we synthesize a scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment that satisfies the specification. In this talk we focus on a two-player continuous-time stochastic game model that we call controller-environment games that is the crucial step in the solution of the problem above.

Highlights Conference 2013 Conference Abstract

The quest for minimal quotients for probabilistic automata

• Christian Eisentraut
• Holger Hermanns
• Johann Schuster
• Andrea Turrini
• Lijun Zhang

Highlights Conference 2013 Conference Abstract

Verification of open interactive Markov chains

• Tomáš Brázdil
• Holger Hermanns
• Jan Krčál
• Jan Kretinsky
• Vojtĕch Řehák

We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property and an IMC component, we synthesize its scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment. We also give a specification formalism for IMC and consider unknown environments satisfying a given specification.

I&C Journal 2011 Journal Article

Probabilistic Logical Characterization

• Holger Hermanns
• Augusto Parma
• Roberto Segala
• Björn Wachter
• Lijun Zhang

Probabilistic automata exhibit both probabilistic and non-deterministic choice. They are therefore a powerful semantic foundation for modeling concurrent systems with random phenomena arising in many applications ranging from artificial intelligence, security, systems biology to performance modeling. Several variations of bisimulation and simulation relations have proved to be useful as means to abstract and compare different automata. This paper develops a taxonomy of logical characterizations of these relations on image-finite and image-infinite probabilistic automata.

I&C Journal 2005 Journal Article

Axiomatising divergence

• Markus Lohrey
• Pedro R. D’Argenio
• Holger Hermanns

When a process is capable of executing an unbounded number of non-observable actions it is said to be divergent. Different capabilities of an observer to identify this phenomena along the execution leads to different divergent sensitive semantics. This paper develops sound and complete axiomatisations for the divergence sensitive spectrum of weak bisimulation equivalence. The axiomatisations separates the axioms concerning recursion and those that capture the essence of diverging behaviour.

I&C Journal 2005 Journal Article

Comparative branching-time semantics for Markov chains

• Christel Baier
• Joost-Pieter Katoen
• Holger Hermanns
• Verena Wolf

This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship.

TCS Journal 2005 Journal Article

Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes

• Christel Baier
• Holger Hermanns
• Joost-Pieter Katoen
• Boudewijn R. Haverkort

A continuous-time Markov decision process (CTMDP) is a generalization of a continuous-time Markov chain in which both probabilistic and nondeterministic choices co-exist. This paper presents an efficient algorithm to compute the maximum (or minimum) probability to reach a set of goal states within a given time bound in a uniform CTMDP, i. e. , a CTMDP in which the delay time distribution per state visit is the same for all states. It furthermore proves that these probabilities coincide for (time-abstract) history-dependent and Markovian schedulers that resolve nondeterminism either deterministically or in a randomized way.

TCS Journal 2002 Journal Article

Process algebra for performance evaluation

• Holger Hermanns
• Ulrich Herzog
• Joost-Pieter Katoen

This paper surveys the theoretical developments in the field of stochastic process algebras, process algebras where action occurrences may be subject to a delay that is determined by a random variable. A huge class of resource-sharing systems – like large-scale computers, client–server architectures, networks – can accurately be described using such stochastic specification formalisms. The main emphasis of this paper is the treatment of operational semantics, notions of equivalence, and (sound and complete) axiomatisations of these equivalences for different types of Markovian process algebras, where delays are governed by exponential distributions. Starting from a simple actionless algebra for describing time-homogeneous continuous-time Markov chains, we consider the integration of actions and random delays both as a single entity (like in known Markovian process algebras like TIPP, PEPA and EMPA) and as separate entities (like in the timed process algebras timed CSP and TCCS). In total we consider four related calculi and investigate their relationship to existing Markovian process algebras. We also briefly indicate how one can profit from the separation of time and actions when incorporating more general, non-Markovian distributions.