ABSTRACT. We study the conditions under which monadic second-order (MSO) interpretations can be simplified by replacing representations of elements as tuples of arbitrary sets with representations as tuples of finite sets or points. Using reparameterizations of MSO formulas, we prove that for formulas with free finite-set variables, it is decidable whether a point reparameterization exists, and that such a reparameterization can be effectively constructed over countable chains. Moreover, over countable Dedekind-complete labeled chains, a formula with free arbitrary set variables admits a finite-set reparameterization if and only if it has at most countably many satisfying assignments. These results yield effective simplification procedures for MSO interpretations over broad classes of countable linear orders.

ABSTRACT. We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form 2n3 − 5n + 3, etc.) Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables. In the case of single-variable theories, we obtain positive results for the following two families of predicates: (i) for perfect fixed powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations; and (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves. Finally, we discuss limitations and hardness results (via encodings of longstanding open Diophantine problems) as soon as any of the above restrictions are lifted.

ABSTRACT. Assume a pair of logical formulae φ,ψ such that φ entails ψ. A *Craig interpolant* is a third formula θ such that: (i) φ entails θ and θ entails ψ, and moreover (ii) θ only uses symbols which appear both in φ and in ψ.

I will discuss recent developments related to the question: how to (efficiently) compute an interpolant for given φ,ψ, if it exists. I will focus on a new technique which enables elementary interpolant construction in (variants of) modal logic with nominals, i.e. an extension of modal logic by predicates which are guaranteed to be true about exactly one element of a model.

Based on joint work with J. C. Jung and F. Wolter.

ABSTRACT. We introduce clique-guarded first-order logic with counting (cgFOC), a fragment of the first-order logic with counting FOC [Kuske and Schweikardt, LICS 2017], and we study the complexity of this fragment. In particular, we prove computable upper bounds on the Vapnik–Chervonenkis (VC) dimension of cgFOC formulas and on the graph dimension of cgFOC counting terms on nowhere dense classes of relational structures. Furthermore, we show algorithmic metatheorems for cgFOC for query answering, enumeration, and probably approximately correct (PAC) learning for Boolean and multiclass classification problems on classes of locally bounded expansion. On the other hand, we show that a slight extension of cgFOC is already intractable on trees.

This is joint work with Steffen van Bergerem and Nicole Schweikardt.

ABSTRACT. A graph class is k-WQO if its k-labeled graphs are well-quasi-ordered under label-preserving induced subgraph embeddings. We show that every hereditary graph class that is 2-WQO has bounded clique-width. Combined with the recent result of Dumas and Lopez, this confirms a long-standing conjecture of Pouzet: A hereditary graph class is 2-WQO if and only if it is k-WQO for all k ≥ 2.

This is joint work with Julien Duron and Nikolas Mählmann.

ABSTRACT. We introduce a new logic, called cluster first-order logic, a restricted fragment of first-order logic specifically designed to study order invariance. An order-invariant formula is one on a vocabulary that contains an order; however, whether a structure satisfies it or not is independent of the interpretation of the order. We show that while order-invariant cluster first-order logic can define properties outside the scope of plain first-order logic in general, its expressive power is included in that of first-order logic when it comes to classes of bounded degree. We establish this result by explicitly constructing linear orders such that similar structures remain similar when they are expanded with these orders. This similarity-preserving, local-to-global approach is technically involved and somewhat counterintuitive, since adding an order usually reveals distinctions that are otherwise hidden due to the locality of first-order logic. We believe that this work can be a stepping stone toward applying such techniques to plain first-order logic and toward settling the question of the expressive power of order-invariant plain first-order logic.

ABSTRACT. In Complex Event Recognition (CER) queries are defined over sequential data to detect specific event patterns. A core feature of CER languages is the interplay between correlation and sequencing, which closely relates to join operations in relational databases. Viewing join evaluation over time-ordered data through this lens reveals a connection to query evaluation under updates, a topic studied in database systems under the umbrella of Dynamic Query Evaluation (DQE).

In this work, we introduce Join Queries with Insertion Order (JQ+IO) as a natural extension of join queries to event streams. We characterise which JQ+IO queries can be evaluated using the General Dynamic Yannakakis join processing framework of Idris et al. (2020) and which can be translated into the CER automata model of Pinto et al. (2025). We further show that these two classes intersect, providing the first formal connection between previously separate lines of work and clarifying their expressiveness with respect to JQ+IO.

To complement our results on expressiveness, we use our characterisations to translate the algorithmic results from CER and generalized join queries, thereby identifying subclasses of acyclic JQ+IO queries that can be maintained over streams under the sliding-window and insertion-only settings. Furthermore, we provide a lower bound on the complexity of enumeration-based query processing under updates, showing that even hierarchical join queries with insertion order can be hard to evaluate in this setting whereas without input order such queries are known to be easy.

ABSTRACT. Index problem asks if the given language can be recognised by an automaton of a given index. The decidability status of this problem for non-deterministic parity automata over infinite trees is still open. Nevertheless, it is generally assumed that the problem should be decidable, we just lack appropriate techniques to prove it.

During my talk I will introduce Index Quantifiers - a translation of the index problem into the syntactic realm of MSO. A single outermost use of an index quantifier is literally equivalent to index problem. However, index quantifiers can be nested...

The main technical result of the talk is undecidability of MSO+index quantifiers over infinite trees. This is joint work with Denis Kuperberg, Damian Niwiński, and Paweł Parys, as presented at STACS 2026 in Grenoble.

ABSTRACT. In 1982, Hauser reformulated a Hankel-style characterisation of regular languages using the communication complexity framework of Yao and Abelson. We propose a generalisation of this protocol for arbitrary relational structures which aims to combine both compositionality and logical definability. In our setting, both of the parties receive a part of the input and transform it using unlimited computational power. Next, the local outputs are combined by an aggregator, and the result is computed by applying an FO-formula to the combined structure. We show that our model is equivalent to Hauser’s on strings and explore its expressivity on general graphs.

This is a joint work with Julien Duron, Thomas Filasto, and Rafał Stefański.

ABSTRACT. Indexed languages are a classical notion in formal language theory, with several characterizations, for instance as the languages of second-order pushdown automata or indexed grammars. The downward closure of a language—the set of all (scattered) subwords of its members—is well-known to be a regular over-approximation, useful in many contexts.

In a recent work with Richard Mandel and Georg Zetzsche, we study the problem of computing the downward-closure of a given indexed language. We show a triply exponential construction of a nondeterministic finite automaton recognizing the downward closure of a given indexed language, together with a matching lower bound.

In this talk I will begin by introducing indexed grammars and discuss pumping techniques that motivate our approach to downward-closure computation. I will then survey what is currently known about downward-closure computation for infinite-state systems, and discuss some open problems in the area.

ABSTRACT. Nested counter systems (NCS) are a generalization of counter systems to higher-order counters. Here, a higher-order counter is allowed to have other (lower-order) counters as elements, instead of just a number. Such systems can be viewed as working on trees, where the height of the tree naturally corresponds to the highest order counter that the system is working with. It is known that the coverability problem for NCS, which asks if a given final tree can be covered from a given initial tree, is $F_{\epsilon_0}$-complete. Here $F_{\epsilon_0}$ is a class in the fast-growing hierarchy of complexity classes.

In this contribution, we consider an extension of NCS called nested reset counter systems (NRCS) that extends NCS with resets. We show that coverability for NRCS over order-$k$ counters is $F_{\Omega_k}$-complete where $\Omega_k$ is the tower of height $k$ of the $\omega$ ordinal. This gives the first natural hierarchy of complete problems for all of these classes. Furthermore, to prove our upper bounds, we also develop length function theorems for any fixed amount of applications of the multiset operation on finite sets.

As an application of our results, we improve existing upper bounds for various problems from XML processing, graph transformation systems, $\pi$-calculus, logic and parameterized verification. Furthermore, using our completeness results for $k$-NRCS, we also prove $F_{\Omega_k}$-completeness of the considered problems from the realms of parameterized verification and logic, for all $k$.

This is joint work with Franzisco Schmidt and has been accepted for publication at LICS 2026.

ABSTRACT. Visibly pushdown automata are a restricted model of pushdown automata which enjoy good properties similar to finite automata. While the language defined by a visibly pushdown automaton can hardly be regular, we can study the decision problem whether it is the restriction of a regular language to the set of well-matched words. This is known to be decidable in elementary time (Bárány, Löding, Serre 2006) but only P-hard, leaving a big gap in complexity. The problem is closely related to the weak validation problem (Segoufin, Vianu 2002), whose decidability status is still unknown.

I will present ongoing work towards proving that the problem can be solved in polynomial-time. In particular, we show how to efficiently test if a visibly pushdown automaton defines a visibly counter language, and if a visibly counter automaton defines a regular language restricted to well-matched words.

(joint work with Annika Delb and Moses Ganardi)

ABSTRACT. Many real-world systems are naturally modelled as infinite-state systems and their automated verification is a challenging problem. We propose a novel framework that yields anytime algorithms for the \emph{quantitative} verification of weighted pushdown systems. We further define a novel class of $\omega$-semirings for which our algorithm guarantees termination. Previously known verification procedures have considered strictly stronger semirings. We exemplify our approach by obtaining an anytime algorithm computing the downward closures for pushdown systems, by instantiating the class of downward-closed languages as an $\omega$-semiring. Using this result, we propose a novel anytime algorithm for the quantitative verification of acyclic weighted pushdown networks which is inherently parallelizable.

This is joint work with David Basin.

ABSTRACT. The reachability problem in multi-pushdown automata (MPDA), or equivalently, interleaved Dyck reachability, has many applications in static analysis of recursive programs. An example is safety verification of multi-threaded recursive programs with shared memory. Since these problems are undecidable, the literature contains many decidable (and efficient) underapproximations of MPDA.

A uniform framework that captures many of these underapproximations is that of _bounded treewidth_: To each execution of the MPDA, we associate a graph; then we consider the subset of all graphs that have a treewidth at most _k_, for some constant _k_. In fact, bounding treewidth is a generic approach to obtain classes of systems with decidable reachability, even beyond MPDA underapproximations. The resulting systems are also called _MSO-definable bounded-treewidth systems_.

While bounded treewidth is a powerful tool for reachability and similar types of analysis, the word languages (i.e. action sequences corresponding to executions) of these systems remain far from understood. For the slight restriction of bounded _special treewidth_, or “bounded-stw” (which is equivalent to bounded treewidth on MPDA, and even includes all bounded-treewidth systems studied in the literature), this work reveals a connection with multiple context-free languages (MCFL), a concept from computational linguistics. We show that the word languages of MSO-definable bounded-stw systems are exactly the MCFL.

We exploit this connection to provide an optimal algorithm for computing _downward closures_ for MSO-definable bounded-stw systems. Computing downward closures is a notoriously difficult task that has many applications in the verification of complex systems: As an example application, we show that in programs with dynamic spawning of MSO-definable bounded-stw processes, safety verification has the same complexity as in the case of processes with sequential recursive processes.

Joint work with C Aiswarya, Pascal Baumann, Prakash Saivasan, and Georg Zetzsche

ABSTRACT. This presentation is about automata equipped with both natural- and integer-valued counters that can be incremented and decremented but cannot be tested for zero (denoted VASS+Z). The focus will be on the reachability problem for 1-VASS+Z and 2-VASS+Z; these automata have one and two natural-valued counters, respectively, as well as any number of integer counters. The first goal of this presentation is to share the key ideas in the relatively simple, robust proof that reachability in binary-encoded 1-VASS+Z is in NP. The second goal of this presentation is to show intriguing techniques that we developed to prove that reachability in unary-encoded 2-VASS+Z is PSPACE-hard.

This presentation concerns a part of joint work with Clotilde Bizière, Wojciech Czerwiński, Roland Guttenberg, Jérôme Leroux, Vincent Michielini, Łukasz Orlikowski, and Antoni Puch accepted into LICS'26.

ABSTRACT. Typically problems for Vector Addition Systems with States (VASS) are parametrized by its number of counters (let us denote it by d). I will analyse another parameter called geometric dimension g, which is the dimension of the linear space spanned by effects of cycles in VASS. Notice that clearly g ≤ d. It was recently noticed that the current best algorithm for the reachability problem in VASS working in F_d also works in F_g, so substantially better if g is much smaller than d. I will present results showing that the current best known results for other classical problems, namely coverability, boundedness, simultaneous unbdoundedness and integer reachability also behave similarly when parametrised by g instead of being parametrised by d. The presentation is based on the paper accepted to ICALP 2026, co-authored by Roland Guttenberg, Łukasz Orlikowski, Henry Sinclair-Banks and Yangluo Zheng.

ABSTRACT. Data Vector Addition Systems with States (data VASS) is an extension of plain Vector Addition Systems with States (VASS) for which the decidability status of the reachability problem is still open. We show decidability of the integer reachability problem (the counters can drop below zero), and believe this result to be a major step towards solving proper reachability. Integer reachability in data VASS is way more complex than in plain VASS (where it is reducible to integer linear programming), mostly due to the fact that the state spaces are not finite but orbit-finite. Our solution combines an iterative decision procedure, inspired by the KLM decomposition in plain VASS, with new techniques for proving termination. As corollaries, we can deduce decidability of the nonemptiness of intersection of Parikh images of register automata, and of the reachability problem for data T-nets (a structural restriction of data Petri nets, a model equivalent to data VASS).

This is a joint work with Sławomir Lasota and Roland Guttenberg.

ABSTRACT. The reachability problem for Vector Addition Systems (VAS) admits two fundamentally different decidability proofs. The classical KLM approach relies on a structural decomposition of runs and yields the optimal Ackermannian complexity bounds. A more recent approach due to Leroux is based instead on inductive invariants: whenever a target configuration is not reachable, there exists a semilinear set containing the source configuration, closed under the transitions of the system, and excluding the target. Decidability then follows by combining an enumeration of runs with a search for such invariants. The proof of existence of these inductive invariants itself splits into two parts. The first establishes geometric properties of VAS reachability sets, namely that they are almost semilinear. The second shows that transition systems with almost semilinear forward and backward reachability sets admit semilinear inductive invariants.

Branching Vector Addition Systems (BVAS) extend VAS with branching transitions allowing to sum two reachable configurations. As a consequence, computations are tree-shaped rather than word-shaped. Their reachability problem has remained open for more than thirty years, since the model was first introduced by Rambow in 1994 and later rediscovered independently by de Groote, Guillaume, Salvati, Verma and Goubault-Larrecq in 2003-2004.

Joint work with Jérôme Leroux and Grégoire Sutre aims at extending the inductive invariant approach to BVAS. We first showed that BVAS reachability sets are sections of VAS reachability sets, and therefore inherit their geometric properties (published at FoSSaCS 2026). However, this does not by itself yield inductive invariants. Indeed, Leroux’s argument relies crucially on VAS being symmetric (taking the opposite of every action in a VAS V yields a reversed VAS V' such that runs from s to t in V correspond to runs from t to s in V'). This symmetry breaks down in the branching setting. We therefore revisited the VAS invariant argument so that it no longer depends on this symmetry property (submitted), and finally extended the construction to BVAS (currently being written up).