ABSTRACT. Transformers are revolutionary neural networks architecture, which has been the backbone of our modern Large Language Models (LLMs). Despite the success of transformers in practice, we often do not know why they work (or occasionally also, why they do not work). Recent years have witnessed rapid progress in understanding transformers through the lens of logic and automata (in the community called FLaNN = Formal Languages and Neural Networks). In particular, the toolbox from logic and automata (i.e. connections to linear temporal logic) has helped us understand why PARITY (and in general “state-tracking”) is difficult for transformers. I will recount some of the fundamental results in the field and open problems at the intersection of logic, automata, verification and transformers. I will also discuss new architectures including state-space models ( more generally linear RNNs), and how these compare in expressiveness to transformers.

This talk is based on recent publications (including at ICLR'24, ICLR'26, and ICML'26).

ABSTRACT. In the theory of games on infinite-state arenas, there is a stark contrast between (i)~recursion-based models such as pushdown systems and extensions on one hand, and (ii)~counter-based models like vector addition systems with states (VASS) on the other. For pushdown systems and extensions, there is a rich variety of decidable and well-understood games, whereas on VASS arenas, even extremely simple games are undecidable. Here, a VASS is an automaton with counters that can be incremented and decremented, but not tested for zero. Crucially, the counters can only assume non-negative values.

However, certain VASS games become decidable when using energy semantics: An energy game is played on a system with counters, but the arena includes configurations with negative counters. The requirement that the counters stay non-negative is, instead, part of the winning condition of the existential player.

We study an analogue of energy semantics---legality of instructions as part of the winning condition rather than arena---on a broad class of infinite-state systems, where we call them viability games. Specifically, we study viability games in the framework of valence systems over graph monoids, where (undirected, loops allowed) graphs specify various infinite-state systems, such as pushdowns, VASS counters, integer counters, and combinations thereof.

In our main results, we provide a complete description of the decidability and complexity landscape of viability games across valence systems over graph monoids. Our results reveal encouraging decidability properties. For example, in certain combinations of pushdowns and counters, viability games are decidable, despite non-termination games being undecidable there. Moreover, viability games are even decidable for certain systems where (single-player) control-state reachability is undecidable.

This presentation is based on joint work with Georg Zetzsche, published at ICALP 2026.

ABSTRACT. Existing studies of multiplayer games on graphs frequently focus on specific numerical reward functions. In this talk, we propose a unifying automata-based approach where player preferences are instead modeled as ω-automatic relations, given by synchronous deterministic parity automata. This flexible framework seamlessly captures classical objectives alongside non-standard preference relations, entirely without requiring structural order assumptions. To map the computational landscape of these games, we redefine the concept of value, not as a scalar, but as the set of plays a player can guarantee to improve upon, recognized by an alternating parity automaton of polynomial size. Building on this construction for multiplayer games, we establish that deciding the existence of a constrained Nash Equilibrium is PSPACE-complete. Finally, we show that for rational synthesis, the cooperative case is PSPACE-complete, while the non-cooperative case becomes undecidable. This is a joint work with Véronique Bruyère, Emmanuel Filiot, and Jean-François Raskin.

ABSTRACT. We study the problem of generating paths on a graph that satisfy a collection of omega-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler---oblivious to the graph and objective---dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions---simple, a priori restrictions agreed upon before the graph or objectives are revealed---that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of omega-regular objectives. In particular, B\"uchi objectives admit universal composition of finite-memory policies without scheduler communication; co-B\"uchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.

This is a joint work with Guy Avni, Thomas A. Henzinger, Kaushik Mallik, and K. S. Thejaswini, published at CAV'26.

ABSTRACT. In the field of automata over infinite words, a long-standing objective has been to define universal automata: an automaton $U_L$, recognizing an $\omega$-regular language $L$, such that any automaton recognizing $L$ (or possibly a sublanguage) admits a morphism towards $U_L$. Some progress has recently been made towards this objective, with the rerailing automata or more particularly the layered automata. We introduce the class of structurally Adam-positional automata. Intuitively, they are automata with an $\omega$-regular set $W$ of accepting paths, that notably satisfy that if two cycles $\rho$, $\rho'$ around a same state are accepting when repeated infinitely often, so is the cycle $\rho\rho'$. Notably, the Streett automata are structurally Adam-positional. We establish that for all prefix-independent languages $L$, there exists a structurally Adam-positional automaton $U_L$ with the following universality property: for all structurally Adam-positional automaton $A$ recognizing some language $L' \subseteq L$, there exists a transition-to-transition morphism from $A$ to $U_L$ that preserves the accepting paths. Notably, $U_L$ is history-deterministic. This is a joint work with Thomas Colcombet.

ABSTRACT. This talk is based on joint work in progress with Mickael Randour, Matéo Torrents and Pierre Vandenhove.

Stochastic zero-sum two-player games on finite graphs model reactive systems as interaction between the controller (Player 1) and the environment. The decisions of the environment are either antagonistic or stochastic, modeled by actions chosen by the opponent Player 2 or chosen randomly from a stochastic vertex. For a given objective, the value of a vertex is the supremum probability that Player 1 can produce a play satisfying the objective starting from the vertex, no matter how the other player plays.

An optimal strategy (for Player 1) specifies how Player 1 can choose actions to win with probability equal to the value of the starting vertex. Memory requirements for optimal strategies have been studied for both stochastic games and deterministic games (no stochastic vertices). In this work, we are interested in relating the memory requirements of stochastic games and deterministic games. Our results can be used to transfer results on memory requirements in deterministic games to results on memory requirements on stochastic games.

For omega-regular objectives admitting a neutral letter, we first show that the memory requirements of strategies to win almost-surely (i.e., with probability 1) in stochastic games is the same as in deterministic games. For strategies achieving the optimal value, we show that additional information about the Myhill-Nerode classes, that identifies the set of winning continuations, is also necessary. Conversely, we show that a product of the Myhill-Nerode automaton and the minimal memory structure for deterministic games suffices to play optimally in stochastic games.

ABSTRACT. We consider two-player games on graphs. A primary application is reactive synthesis, in which the goal is to design a reactive system that ensures the specification in any environment. Synthesis is solved by constructing a two-player graph game between a system player and an environment player, who is traditionally adversarial, modelling no assumptions being made on the environment. In many situations, however, some information about the environment is available. For example, consider the task of designing a controller for a vehicle that approaches an intersection, where another vehicle approaches from the left and can apply one of two actions: continue straight, in which case the intersection is occupied, or turn right, in which case it is free. We introduce and study color-restricted adversary (CRA) games that can incorporate such assumptions on the environment. Each one of the opponent's strategies in a CRA game is associated with a color, and the opponent is restricted to follow one of these strategies. The proponent thus ``rules out'' colors as the game develops; when the opponent chooses an action that does not comply with a strategy, the strategy is ruled out. We consider a special case in which the color uniquely determines the next action (UCRA) as is the case in the vehicle example. We first study an adversarial choice of colors and show that deciding the winner is PSPACE-complete in CRA games and NP-complete in UCRA games. We consider UCRA games in which the opponent selects their color according to a known probability distribution and reduce the problem of finding the value of the game to an integer linear program. Finally, we study the problem of finding an optimal mixed strategy for the proponent.

ABSTRACT. Higher Dimensional Automata are a very powerful model of concurrency to represent truly parallel events, i.e. events that happen simultaneously. They are therefore more expressive than classical automata by allowing non-interleaving concurrency. In this work, we extend classical notions of games on graphs to Higher DimensionalAutomata: games are represented by an arena where several players coexist (some of whom may be allies) with (possibly different) objectives, as accessibility or safety.

ABSTRACT. The Büchi-Landweber theorem establishes decidability and effective synthesis of winning strategies in regular infinite games played on finite arenas. In this work, we generalise this theorem to games whose arenas are infinite words. The setting is as follows. There is a fixed infinite word p (a parameter). For each position, Player I and then Player II produce one additional letter, yielding a word with three tracks: the parameter track and one track for each player. Finally, to find a winner, we check whether the word belongs to some regular language W. An equivalent formulation is given in terms of game quantifiers.

We obtain results on three levels. First, deciding the winner: given the regular winning condition W, one can construct a regular language of those parameter words p over which Player II can win. Second, synthesis of finite-memory strategies: based on W, one can construct a finite-memory transducer equipped with regular lookahead on the parameter word p, which generates a winning strategy of Player II. Third, elimination of lookahead in the special case of separated winning conditions: if the winning condition is a Boolean combination of languages depending only on the parameter track and Player I's track, and languages depending only on Player II's track, then a winning strategy of Player II can be generated by a finite-memory transducer without any lookahead (while in general some lookahead is necessary).

The winner determination result is folklore and follows from work of Kaiser. The next two results are novel. The key step for the second result is uniformisation of MSO formulae, which allows us to select a particular winning strategy, and then to synthesise it. For the third result, we work with Wilke algebras to obtain a constructive variant of Ramsey's theorem, building on a technical idea due to Thomas.

This presentation is based on the paper Generalised Quantifiers Based on Rabin-Mostowski Index published on STACS 2026; co-authors: Denis Kuperberg, Damian Niwiński, Michał Skrzypczak.

ABSTRACT. In this work we introduce the notion of a runtime consultant. A runtime consultant is defined with respect to some value function on infinite words. Similar to a runtime monitor, it runs in parallel to an execution of the system and provides inputs at every step of the run. While a runtime monitor alerts when a violation occurs, the idea behind a consultant is to be pro-active and provide recommendations for which action to take next in order to avoid violation (or obtain a maximal value for quantitative objectives). It is assumed that a runtime-controller can take these recommendations into consideration. The runtime consultant does not assume that its recommendations are always followed. Instead, it adjusts to the actions actually taken (similar to a vehicle navigation system). We show how to compute a runtime consultant for common value functions used in verification, and that almost all have a runtime consultant that works in constant time. We also develop consultants for omega-regular properties, under both their classical Boolean semantics and their recently proposed quantitative interpretation. This is joint work with Dana Fisman, previously presented at RV 2025; the paper is available at https://link.springer.com/chapter/10.1007/978-3-032-05435-7_27

ABSTRACT. We consider symbolic omega-automata, i.e., automata over an alphabet of valuations of variables over possibly infinite domains. Typical approaches to retain information from past symbols rely on registers or memory cells, usually at the cost of rather intricate semantics.

We propose a slightly different approach based on obligations, i.e., assignment-like constructs attached to transitions, reminiscent of "next-state" constraints in SMV. Intuitively, whenever a transition with an obligation is taken, the obligation is evaluated on the current symbol and yields a constraint on the next symbol that the automaton will read. Thus, the effect of an obligation is ephemeral, compared to the persistent write operations in register automata.

We show the semantics of obligation automata with Emerson-Lei acceptance to be rather intuitive, when compared to, say, register automata. Although emptiness is undecidable in general we propose a semi-algorithm for emptiness, and discuss classes of obligation automata under which it is guaranteed to terminate. We can also generalise the semantics to support universal branching.

We also have a prototype implementation that supports several operations on these automata, by reusing Spot and IC3IA (an efficient IC3 model checker, used for emptiness checking).

ABSTRACT. Higher Dimensional Automata (HDA) are a very expressive model of true concurrency, derived from and generalizing classical automata. Its associated language is interval partially ordered multisets with interface (iiPomset). In this work, we study notions of distance and topology on iiPomsets in order to introduce verification in HDAs, via quantitative model-checking and robustness. Joint work with Emily Clement and Maya Hayman.

ABSTRACT. Lagrangian-based duality, traditionally applied in optimization, has recently been generalized to serve as the basis for a unifying framework for primal-dual search algorithms in the context of program verification and automated reasoning.

In this paper, we analyze Quantified Satisfiability Modulo Theories (QSMT) algorithms using this framework. Interestingly, our Lagrangian-based analysis reveals that three recently proposed algorithms for quantified linear real arithmetic (LRA) share a common structure, and that their main differences lie in the approach to a certain problem—model-based projection for ∃∀-formulas.

Moreover, in the course of this Lagrangian-based analysis, we identify an issue with the progress property of one of the algorithms, propose a way to fix the issue, and experimentally demonstrate that the proposed fix improves performance.

This work has been accepted to the 38th International Conference on Computer Aided Verification (CAV 2026).

Co-Authors: Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham

ABSTRACT. Automated theorem provers like Vampire are effective at finding proofs in first order logic, but validating these proofs by more trustworthy programs (like interactive theorem provers or verified proof checkers) is increasingly demanded to establish trust. To address this, our recent paper (accepted at ITP 2026) introduces a method for reconstructing Vampire's output in Lean (interactive theorem prover) which can check the proofs end-to-end. The approach systematically translates Vampire's preprocessing steps and core inference rules as well as extended proof search like AVATAR into Lean theorems that are subsequently validated in Lean's kernel. The approach achieves a 99% success rate in checking proofs for CNF and FOF problems from the TPTP library within selected timeout and memory limits, showing the applicability of the approach. Building upon this work, a currently under-development system extends this capability to verify generic TSTP proofs from other automated theorem provers by utilizing Vampire as a proof-reconstruction intermediary. Ultimately, these advancements significantly reduce the trusted computing base for automated reasoning by handing off final proof validation to Lean's Kernel.

Co-Authors: Márton Hajdu, Laura Kovács, Axel Polaczek and Michael Rawson

ABSTRACT. Separation logic (SL) is one of the most popular formalisms for reasoning about programs that manipulate dynamically allocated memory. Although many decision procedures for SL have been proposed, existing solvers are usually not used by verifiers, which instead rely on custom heuristics. One of the main reasons is the lack of support for combining SL reasoning with other SMT theories. Attempts to bridge this gap rely on translating SL into SMT, but existing approaches support only a limited class of inductive predicates with built-in semantics. This talk presents ongoing work on the first translation of SL to SMT supporting a rich fragment of user-defined inductive definitions. The decision procedure relies on a small-model property, established through an automata-based argument, combined with incremental unfolding of inductive definitions, which leverages the power of incremental SMT solvers.

The talk presents a joint work with Tomáš Vojnar (Brno University of Technology and Masaryk University), Adam Rogalewicz (Brno University of Technology), Florian Zuleger (TU Wien) and Mihaela Sighireanu (ENS Paris-Saclay).

ABSTRACT. The landscape of automated formal verification is populated by techniques that make markedly different trade-offs. Some focus on expressiveness and precision, such as Java Pathfinder, which supports LTL-style property checking by modifying the JVM to systematically explore executions. Others favor scalability and practicality so that they can be applied to larger programs using diverse language features, such as the Java Deadlock Analyzer (JaDA), which employs a type system whose types describe synchronization and dependency behavior. This talk presents Petrify, a novel automated verification technique for concurrency properties that achieves a distinctive trade-off. Petrify encodes the semantics of Java bytecode programs into Petri nets (PNs), which can then be analyzed by state-of-the-art model checking tools such as LoLA. As our experiments demonstrate, Petrify offers an attractive combination of expressiveness and practicality: PNs provide a fairly precise encoding of program concurrency, while Petrify's PN representation remains compact, making the analysis largely insensitive to parameter size. Other authors: Carlo A. Furia (USI, Lugano)

ABSTRACT. I will talk about the first fully automated framework for precise reasoning about parameterized quantum circuits. The framework uses a special flavor of weighted tree transducers to capture the semantics of a practically relevant class of quantum circuits parameterized by the number of qubits, such as implementations of Bernstein-Vazirani's algorithm, the loop body of Grover's algorithm, or circuits for parameterized simulation of certain Hamiltonians. Our framework guarantees decidability of equivalence checking and relational pre/post-condition verification of parameterized circuits that can be expressed by the formal model.

This is a joint work with Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hečko, Lukáš Holík, Jyun-Ao Lin, and Ramanathan S. Thinniyam.