Seminars

Symbolic Probabilistic model checking is a formal verification technique for systems with stochastic behaviour. In this talk we will introduce the key building blocks: fundamentals of Binary Decision Diagrams (BDDs) and their operations, their extension to Multi-Terminal BDDs (MTBDDs) as a representation for stochastic matrices, and how these concepts underpin symbolic probabilistic model checking.

In his PhD project "Teacher Empowerment for Artificial Intelligence," Wolfgang Robinig investigates how teachers can be prepared to teach AI effectively. The research includes a survey on current AI understanding and usage as well as professional development needs, the creation of teaching materials, and an experience report from his own teaching practice. Current work focuses on identifying the most relevant subfields of AI for teacher education, as well as a framework on (teaching about) biases in AI.

Correctness-Guided Reinforcement Learning refers to a methodology that integrates formal verification into the training process of Reinforcement Learning (RL) agents to ensure safety in probabilistic environments. Traditional RL often struggles with safety because it optimizes for a single reward signal. For this matter, reward shaping is often used to encode the safety behavior into the reward signal. However, this is hard and it provides no explicit bounds on safety. A remedy is constrained RL, where a cost signal is additionally introduced. This talk covers a two-phase framework designed to internalize safety boundaries through a formally verified, dense cost signal integrated into the constrained RL framework.

The term "Automata Learning" refers to a range of algorithms that seek to infer behavioral models of a Systems under Learning (SuL). This is achieved either actively by interacting with the SuL or passively from a prerecorded set of traces. This talk covers state-merging, which is one of the most prevalent approaches in passive automata learning. In particular, we discuss the red-blue framework, which is at the heart of many state-merging algorithms, such as RPNI for Deterministic Finite Automata and Mealy Machines or IOAlergia for Markov Decision Processes.

Markov decision processes (MDPs) are a fundamental model in planning, reinforcement learning and decision making under uncertainty. Several approaches for solving MDPs rely on sampling paths. This technique has two distinct motivations, depending on the setting: Firstly, if the MDP is fully known, then sampling paths improves scalability, focussing computation on the relevant states. Methods exploiting this idea are called partial-exploration based. Secondly, if we only have limited information about the MDP, in particular not knowing its precise transition function, then sampling paths allows to still solve the MDP while providing a probabilistic guarantee. Algorithms for this setting are called statistical model checking. My talk will explain the ideas underlying and connecting these approaches, as well as highlight the key challenges to be overcome.

In this talk, I tackle the problem of using domain knowledge to improve deep reinforcement learning (RL) policies. I present LEGIBLE, a novel approach, following a multi-step process, which starts by mining rules from a deep RL policy, constituting a partially symbolic representation. These rules describe which decisions the RL policy makes and which it avoids making. In the second step, we generalize the mined rules using domain knowledge expressed as metamorphic relations. We adapt these relations from software testing to RL to specify expected changes of actions in response to changes in observations. The third step is evaluating generalized rules to determine which generalizations improve performance when enforced. These improvements show weaknesses in the policy, where it has not learned the general rules and thus can be improved by rule guidance. LEGIBLE, supported by metamorphic relations, provides a principled way of expressing and enforcing domain knowledge about RL environments. We show the efficacy of our approach by demonstrating that it effectively finds weaknesses, accompanied by explanations of these weaknesses, in eleven RL environments and by showcasing that guiding policy execution with rules improves performance w.r.t. gained reward. Closing the loop from neural to symbolic and back to neural representation, we show how to integrate symbolic (rule-based) knowledge into neural RL policies by leveraging RL from demonstrations.

In a world where systems become increasingly complex, modeling them becomes increasingly important. We can model black-box reactive systems as finite state machines from their observed behavior using passive automata learning. However, sometimes, the modeling power of finite state machines does not suffice. Therefore, in this talk, we will extend automata learning to extended finite state machines. These machines provide more computational power by extending finite state machines with a variable store. We present a novel approach based on SMT and SyGuS to infer extended finite state machines from data and evaluate it on various examples.

For languages over finite words, automata types that permit polynomial-time minimization are well-known. For languages over infinite words, as used when specifying the behavior of reactive systems, finding an automaton class that has a polynomial-time minimization algorithm proved to be substantially more difficult. While some such representations for so-called lasso languages exists, their use in applications is limited and tends to be restricted to language learning. In this talk, we present recent progress towards solving this problem. We start by showing how arbitrary omega-regular languages can be canonically decomposed into a series of co-Büchi languages, each of which can in turn be made canonical and minimized by representing them as history-deterministic co-Büchi automata with transition-based acceptance. We show how to translate such a chain of co-Büchi automata (COCOA) representation into a fixpoint formula for performing reactive synthesis over a game graph. Afterwards, we consider the question if the main ideas of the COCOA representation can be lifted to an automaton model in which the language to be represented is only encoded as a single automaton, as usual in automata theory. We show that a reinterpretation of how history-deterministic co-Büchi automata accept words can be combined with parity acceptance to obtain a polynomial-time minimizable automaton model for arbitrary omega-regular languages. Finally, we show that this new automaton model is useful both for reactive synthesis and probabilistic verification.

Building on the concept of probabilistic model checking from Stefans previous talk, this session introduces the concept of post shielding. We demonstrate its practical applicability through illustrative case studies in the automotive domain, aimed at increasing the safety of pedestrians, using the realistic driving simulator CARLA.

We will continue from the previous seminar by exploring how probabilistic model checking queries are solved. In particular, we will examine how PCTL queries are decided for Markov chains and Markov decision processes.

We will begin by introducing the basics, by focusing on the PRISM modeling language and tool support. We will look at how models and properties can be described in PRISM and how we can analyze models using the Storm model checker and its Python interface, Stormpy.

Two classical notions for assessing the fairness of a static decision maker are individual fairness and group fairness. Individual fairness requires that similar individuals receive similar decisions; group fairness requires that the expected decision be independent of group membership. While both notions are well understood in static settings, their extension to dynamic settings is less clear. In this talk, I discuss how to assess and monitor the fairness of decision sequences at runtime. Although designed for fairness, these monitors have broader utility: the individual fairness monitor, built on nearest-neighbour search, can serve as a robustness monitor for neural networks, and the group fairness monitor, relying on sequential statistical inference, can quantify uncertainty about unobserved model parameters.

Building on Iosifs talk on Structured Argumentation, Andrei will discuss how structural properties - particularly bounded treewidth - can be used to tackle hard reasoning tasks in Assumption-based Argumentation (ABA). The talk will present FPT algorithms (parameterised by treewidth) for verifying an extension in ABA, their implementation in ASP, and preliminary results on instances with bounded treewidth.