Program

This talk looks at explainability, interpretability, verifiability, and other key properties of AI systems. We will discuss how these ideas are reflected in new regulations like the EU AI Act, and how formal methods can help make them more concrete in system design. We will see examples of how techniques like model checking and runtime verification can support building AI systems that meet regulatory requirements.

Logic in Computer Science plays important roles ranging from formal methods to Human-Computer Interaction, including Software and Hardware Engineering, etc. Regarding the former broad application domain of formal methods, a tremendous amount of work concern verification, namely satisfiability checking (for model synthesis) and model checking (for counterexample/witness synthesis). I want to discuss a fairly novel question, called Formula Synthesis Problem, that I believe is extremely natural to address, and yet has not received enough attention in logic. In its most general form, the Formula Synthesis Problem consists in deciding whether some formula in a given set is satisfied by a given model (and output one if any). Obviously, if the input set of formulas is finite, this amounts to model checking. On the contrary, if this set is infinite, say obtained by some tree-grammar for formulas, then the answer becomes extraordinary challenging.

Nondeterminism plays a fundamental role in formal language theory, particularly in finite automata, where it allows more succinct representations of regular languages without increasing expressive power. Another regular language model is two-way automata, which allow the head to move leftward and rightward. However, the precise cost of simulating a nondeterministic two-way automata (2NFA) with a deterministic one (2DFA) has remained a longstanding open problem in the field of descriptional complexity since 1978, known as the Sakoda-Sipser question. In this talk, we introduce a novel form of nondeterminism called common guess. This type of nondeterminism corresponds to colouring in the context of MSO-transduction. In an automaton equipped with common guess (2DFA+cg for short), the machine first nondeterministically annotates the input string and then processes the annotated word deterministically as a standard 2DFA. While this approach does not extend expressive power beyond regular languages, we show that it significantly improves succinctness compared to standard 2NFAs. Additionally, we compare this model with another representation of regular languages, namely 1-limited automata. We discuss how the 2DFA+cg is positioned between 1-limited automata and their deterministic counterparts, offering new insights into the relationship between nondeterminism and determinism in the descriptional complexity of finite automata.

Joint work with Bruno Guillon and Luca Prigioniero.

We introduce the class of lexicographic transductions which are word to word transductions with exponential growth. They subsume most known models of transductions such as polyregular transductions or transductions given by copyful streaming string transducers. We give three equivalent definitions of this class and show it enjoys many nice closure properties.

Feedback allows systems to seamlessly and instantaneously adapt their behavior to their environment and is thereby the fundamental principle of life and technology – it lets animals breathe, it stabilizes the climate, it allows airplanes to fly, and the energy grid to operate. During the last century, control technology excelled at using this power of feedback to engineer extremely stable, robust, and reliable technological systems.

With the ubiquity of computing devices in modern technological systems, feedback loops become cyber-physical – the laws of physics governing technological, social or biological processes interact with (cyber) computing systems in a highly nontrivial manner, pushing towards higher and higher levels of autonomy and self-regulation. True autonomy, however, requires complex strategic and reactive decision making to interact with classical feedback control. While stability, robustness and reliable self-adaptation remain to be of uppermost importance in these systems, the understanding of autonomy-driven strategic feedback loops and their utilization for this purpose is currently lacking behind.

In this talk, I will discuss how a control-inspired view on formal methods, in particular reactive synthesis, holds high promises for the design of robust and adaptable autonomy-driven strategic feedback loops in cyber-physical systems.

Recent years have seen some progress on the language theory of higher-dimensional automata (HDAs). Here we take another point of view and introduce an operational semantics of HDAs in terms of finite automata over a certain infinite graph alphabet. Based on papers presented at RAMiCS'24 and DLT'24.

We study automata weighted over number rings, that is rings of integers in an algebraic number field. Assuming a full representation of a number ring O_K, we obtain an exact learning algorithm of O_K-weighted automata that runs in polynomial time in the size of the target automaton, the logarithm of the length of the longest counterexample, the degree of the number field, and the logarithm of its discriminant. Our algorithm produces an automaton that has at most one more state than the minimal one, and we prove that doing better requires solving the principal ideal problem, for which the best currently known algorithm is in quantum polynomial time.

More generally, we develop a generic reduction procedure for active learning problems. Our approach is inspired by a recent polynomial-time reduction of the exact learning problem for weighted automata over integers to that for weighted automata over rationals (Buna-Marginean et al. 2024), and improves the efficiency of a category-theoretic automata learning algorithm.

A join algorithm is said to be worst case optimal for a class of databases C if the time needed to compute the join is linear in the time needed to output the largest possible join one can have by considering databases from C. Many worst case optimal joins have been proposed in the literature but their analysis is often hard to understand. For some of them, knowledge of the actual value for the worst case is necessary, for others, non trivial data structures are needed. In this talk, we will present a very simple algorithm that achieves worst case optimality in many database classes with a simple analysis that does not depend on the knowledge of the worst case value nor on any kind of data structures. We will show how knowledge of the worst case value can then be leverage in this algorithm to transform it into an algorithm for sampling the answers uniformly with good complexity guarantees, matching the complexity obtained recently in more convoluted way. Our goal is to propose a modular and simple enough approach that can be taught easily.

The most commonly studied problems related to complexity theory are the so-called decision problems. They consist in deciding whether, given an input instance, a certain condition is verified or not. Most often, these problems raise the question of whether there exists a solution or not. For their part, enumeration problems are interested in enumerating all solutions. Enumeration problems have been studied in the context of computational complexity theory, and several complexity classes have been introduced for these problems (for tractable ones, we can cite EnumP, OutputP, IncP, DelayP). Our work aims to bring the mission of descriptive complexity to the world of enumeration. The ultimate goal is to successfully capture a tractable enumeration complexity class (namely IncP) with a certain logic. We will then be able to say that an enumeration problem belongs to this complexity class if and only if there is a formula from this certain logic which expresses this problem. Our exploration will lead us to study fragments of third-order logic and to capture natural enumeration problems.

We consider deterministic games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs. We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of lim sup mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain lim inf total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy. This talk is based on joint work with Rasmus Ibsen-Jensen, David Purser, Patrick Totzke and Pierre Vandenhove and was published at CONCUR 2024.

This talk investigates Nash equilibria (NEs) in multi-player turn-based games on graphs, where player preferences are modeled as ω-automatic relations via deterministic parity automata. Unlike much of the existing literature, which focuses on specific reward functions, our results apply to any preference relation definable by an ω-automatic relation. We analyze the computational complexity of determining the existence of an NE (possibly under some constraints), verifying whether a given strategy profile forms an NE, and checking whether a specific outcome can be realized by an NE. Finally, we explore fundamental properties of ω-automatic relations and their implications in the existence of equilibria and finite-memory strategies.

In this talk, I will consider simple stochastic games with terminal-node rewards and multiple players, who have differing perceptions of risk. Specifically, we study risk-sensitive equilibria (RSEs), where no player can improve their perceived reward – based on their risk parameter – by deviating from their strategy. We start with the entropic risk (ER) measure, which is widely studied in finance. ER characterises the players on a quantitative spectrum, with positive risk parameters representing optimists and negative parameters representing pessimists. Building on known results for Nash equilibira, we show that RSEs exist under ER for all games with non-negative terminal rewards. However, using similar techniques, we also show that the corresponding constrained existence problem – to determine whether an RSE exists under ER with the payoffs in given intervals – is undecidable.

To address this, we introduce a new, qualitative risk measure – called extreme risk (XR) – which coincides with the limit cases of positively infinite and negatively infinite ER parameters. Under XR, every player is an extremist: an extreme optimist perceives their reward as the maximum payoff that can be achieved with positive probability, while an extreme pessimist expects the minimum payoff achievable with positive probability. Our first main result proves the existence of RSEs also under XR for non-negative terminal rewards. Our second main result shows that under XR the constrained existence problem is not only decidable, but NP-complete. Moreover, when all players are extreme optimists, the problem becomes PTIME-complete. Our algorithmic results apply to all rewards, positive or negative, establishing the first decidable fragment for equilibria in simple stochastic games with terminal objectives without restrictions on strategy types or number of players.