We study a cyclic proof system C over regular expression types, inspired by linear logic and non-wellfounded proof theory. Proofs in C can be seen as strongly typed goto programs. We show that they denote computable total functions and we analyse the relative strength of C and Gödel's system T. In the general case, we prove that the two systems capture the same functions on natural numbers. In the affine case, i.e., when contraction is removed, we prove that they capture precisely the primitive recursive functions—providing an alternative and more general proof of a result by Dal Lago, about an affine version of system T.

Holonomic techniques have deep roots going back to Wallis, Euler, and Gauss, and have evolved in modern times as an important subfield of computer algebra, thanks in large part to the work of Zeilberger and others over the past three decades. In this talk, I will give an overview of the area, and in particular will present a select survey of known and original results on decision problems for holonomic sequences and functions. I will also discuss some surprising connections to the theory of periods and exponential periods, which are classical objects of study in algebraic geometry and number theory; in particular, I will relate the decidability of certain decision problems for holonomic sequences to deep conjectures about periods and exponential periods, notably those due to Kontsevich and Zagier.

Parts of this talk will be based on the paper “On Positivity and Minimality for Second-Order Holonomic Sequences”, https://arxiv.org/abs/2007.12282 .

We consider the rational subset membership problem for Baumslag-Solitar groups. These groups form a prominent class in the area of algorithmic group theory, and they were recently identified as an obstacle for understanding the rational subsets of GL(2,ℚ). We show that rational subset membership for Baumslag-Solitar groups BS(1,q) with q ≥ 2 is decidable and PSPACE-complete. To this end, we introduce a word representation of the elements of BS(1,q): their pointed expansion (PE), an annotated q-ary expansion. Seeing subsets of BS(1,q) as word languages, this leads to a natural notion of PE-regular subsets of BS(1,q): these are the subsets of BS(1,q) whose sets of PE are regular languages. Our proof shows that every rational subset of BS(1,q) is PE-regular. Since the class of PE-regular subsets of BS(1,q) is well-equipped with closure properties, we obtain further applications of these results. Our results imply that (i) emptiness of Boolean combinations of rational subsets is decidable, (ii) membership to each fixed rational subset of BS(1,q) is decidable in logarithmic space, and (iii) it is decidable whether a given rational subset is recognizable. In particular, it is decidable whether a given finitely generated subgroup of BS(1,q) has finite index.

This is joint work with Michaël Cadilhac and Dmitry Chistikov.

We show that a polyregular word-to-word function is regular if and only if its output size is at most linear in its input size. Moreover a polyregular function can be realized by: a transducer with two pebbles if and only if its output has quadratic size in its input, a transducer with three pebbles if and only if its output has cubic size in its input, etc. Moreover the characterization is decidable and, given a polyregular function, one can compute a transducer realizing it with the minimal number of pebbles. We apply the result to mso interpretations from words to words. We show that mso interpretations of dimension k exactly coincide with k-pebble transductions.

I will present the tools we used to study tilings that are both substitutive and planar (a relaxed version of cut-and-project) in order to present our main result that there exist planar substitution tilings with 2n-fold rotational symmetry for any odd n.

In this talk we will focus on the so-called control-state reachability problem (also called the coverability problem) for 1-dimensional vector addition systems with states (VASS). We show that this problem lies in NC: the class of problems solvable in polylogarithmic parallel time. We will also generalize the problem to allow disequality constraints on transitions (i.e., we allow transitions to be disabled if the accumulated weight is equal to a specific value). For this generalization, we show that the coverability problem is solvable in polynomial time even though a shortest run may have exponential length.

In the setting of regular languages of infinite words, Good-for-Games (GFG) automata can be seen as an intermediate formalism between determinism and nondeterminism, with advantages from both worlds. Indeed, like deterministic automata, GFG automata enjoy good compositional properties (useful for solving games and composing automata and trees) and easy inclusion checks. Like nondeterministic automata, they can be exponentially more succinct than deterministic automata. I will focus in this talk on the following problem: given a nondeterministic parity automaton on infinite words, is it GFG ? The complexity of this problem is one of the main remaining open questions concerning GFG automata, motivated by the potential applications that would come with an efficient algorithm. After giving the necessary context, I will explain the current understanding on this question, and describe a simple polynomial-time algorithm that is conjectured to solve the problem, but has only been proven correct if the input is a Büchi or a co-Büchi automaton.

I will show that the universality problem is ExpSpace-complete for unambiguous VASS, which is in strong contrast with Ackermann-completeness of the same problem for nondeterministic VASS. I also plan to present some more results concerning the interplay between unambiguity and VASS.

(joint work with Diego Figueira and Piotr Hofman)

We study the universality and inclusion problems L(A)⊆L(B) for register automata over equality data. We show that the universality and inclusion problems can be solved in 2-EXPTIME when both automata A, B are without guessing and B is unambiguous, which improves on the recent 2-EXPSPACE upper bound by Mottet and Quaas. We proceed by reducing inclusion to universality, and then universality to the problem of counting the number of orbits of runs of the automaton. We show that the orbit-counting function satisfies a system of bidimensional linear recursive equations with polynomial coefficients (linrec), which generalises analogous recurrences for the Stirling numbers of the second kind, and then we show that universality reduces to the zeroness problem for linrec sequences. While such a counting approach is classical and has successfully been applied to unambiguous finite automata and grammars over finite alphabets, its application to register automata over infinite alphabets is novel.

We provide two algorithms to decide the zeroness problem for the linrec sequences arising from orbit-counting functions. Both algorithms rely on skew polynomials. The first algorithm performs variable elimination and has elementary complexity. The second algorithm relies on the computation of the Hermite normal form of matrices over a skew polynomial field. This yields an EXPTIME decision procedure for the zeroness problem, which in turn yields the claimed bounds for the universality and inclusion problems of register automata.

We will discuss the expressive and computational power of Ordinary Differential Equations (ODEs). We present the general theory of discrete ODEs for computation theory, we illustrate this with various examples of algorithms, and we provide several implicit characterizations of complexity and computability classes.

In this talk, I will present algorithms to learn deterministic finite automata (due to Angluin) and weigthed automata over the usual semiring R with addition and multiplication (due to Beimel, Bergadano, Bshouty, Kushilevitz and Varricchio). I will then present some related open questions and pinpoint the difficulty that arise when trying to generalise these algorithms to any semiring.

We investigate weighted context-free languages of infinite words, a generalization of ω-context-free languages (Cohen, Gold 1977) and an extension of weighted context-free languages of finite words (Chomsky, Schützenberger 1963). As in the theory of formal grammars, these weighted languages, or ω-algebraic series, can be represented as solutions of ω-algebraic systems of equations and by weighted ω-pushdown automata.

Our results are threefold. We show that ω-algebraic systems can be transformed into Greibach normal form. Our second result proves that simple ω-pushdown automata recognize all ω-algebraic series. Simple pushdown automata do not use ε-transitions and can change the stack only by at most one symbol. We use these results to prove a logical characterization of weighted ω-context-free languages in the sense of Büchi, Elgot and Trakhtenbrot.

This is joint work with Manfred Droste and Werner Kuich.

Abstract: Detectability is a basic property of partially observed dynamic systems. If a system satisfies such a property, then one can use an observed output sequence generated by the system to determine its internal states after some time. This property plays an important role in many problems such as state estimation and controller synthesis. Finite automata and labeled Petri nets are two widely-studied models in discrete-event systems, which consist of transitions between discrete states driven by spontaneous occurrences of events, and can be seen as abstractions of many practical systems. (A supervisory control framework for synthesising controllers in discrete-event systems was initiated by Ramadge and Wonham in the late 1980s.) In this talk, we introduce recent verification results on a particular property called strong detectability, for finite automata and labeled Petri nets, and several related further topics.

The Strahler number is a measure of branching complexity of rooted trees. We define the Strahler number of a parity game to be the the smallest Strahler number of the tree of any of its attractor decompositions. In this talk, we will argue that the Strahler number of a parity game is a robust, and hence arguably natural, parameter: it coincides with its alternative version based on trees of progress measures and— remarkably—with the register number defined by Lehtinen (2018). We will also look at how parity games can be solved in quasi-linear space and in time that is polynomial in the number of vertices n and linear in (d/2k)^k , where d is the number of priorities and k is the Strahler number. This complexity is quasi-polynomial because the Strahler number is at most logarithmic in the number of vertices. This significantly improves the running times and space achieved for parity games of bounded register number by Lehtinen (2018) and by Parys (2020).

The framework of document spanners abstracts the task of information extraction from text as a function that maps every document (a string) into a relation over the document’s spans (intervals identified by their start and end indices). For instance, the regular spanners are the closure under the Relational Algebra (RA) of the regular expressions with capture variables, and the expressive power of the regular spanners is precisely captured by the class of vset-automata - a restricted class of transducers that mark the endpoints of selected spans. In this work, we embark on the investigation of document spanners that can annotate extractions with auxiliary information such as confidence, support, and confidentiality measures. To this end, we adopt the abstraction of provenance semirings by Green et al., where tuples of a relation are annotated with the elements of a commutative semiring, and where the annotation propagates through the (positive) RA operators via the semiring operators. Hence, the proposed spanner extension, referred to as an annotator, maps every string into an annotated relation over the spans. As a specific instantiation, we explore weighted vset-automata that, similarly to weighted automata and transducers, attach semiring elements to transitions. We investigate key aspects of expressiveness, such as the closure under the positive RA, and key aspects of computational complexity, such as the enumeration of annotated answers and their ranked enumeration in the case of numeric semirings. For a number of these problems, fundamental properties of the underlying semiring, such as positivity, are crucial for establishing tractability. This is a joint work with Johannes Doleschal, Benny Kimelfeld and Wim Martens.

Automata for infinite alphabets, despite undeniable appeal, are a bit of a theoretical mess. Almost all models are non-equivalent as language recognisers: deterministic/nondeterministic/alternating, one-way/two-way, etc. Also monoids give a different class of languages, and mso gives yet another.

In this talk, I will describe how the single-use restriction can bring some order into this zoo. The single-use restriction says that once an atom from a register is queried, then that atom disappears. Among our results: a Factorisation Forest Theorem, a Krohn-Rhodes decomposition, and a class of “regular” transducers which admits four equivalent characterisations.

Joint work with Rafał Stefański.

In this paper we show that given a max-plus automaton (over trees, and with real weights) computing a function f and a min-plus automaton (similar) computing a function g such that f ⩽ g, there exists effectively an unambiguous tropical automaton computing h such that f ⩽ h ⩽ g. This generalizes a result of Lombardy and Mairesse of 2006 stating that series which are both max-plus and min-plus rational are unambiguous. This generalization goes in two directions: trees are considered instead of words, and separation is established instead of characterization (separation implies characterization). The techniques in the two proofs are very different.

We investigate the connection between properties of formal languages and properties of their generating series, with a focus on the class of holonomic power series.

It is a classical result that regular languages have rational generating series and that the generating series of unambiguous context-free languages are algebraic. This connection between automata theory and analytic combinatorics has been successfully exploited. For instance, Flajolet used it in the eighties to prove the inherent ambiguity of some context-free languages using criteria from complex analysis.

Settling a conjecture of Castiglione and Massazza, we establish an interesting link between unambiguous Parikh automata and holonomic power series, which also yields characterizations of inherent ambiguity and algorithmic byproducts for these automata models.

This is a joint work with Alin Bostan, Arnaud Carayol and Cyril Nicaud.

Finite automata pose an interesting alternative way to present groups and semigroups. Some of these automaton groups became famous for their peculiar properties and have been extensively studied. In addition to that, there exists also a line of research on the general properties of the class of automaton groups.

One aspect of this research is the study of algorithmic properties of automaton groups and semigroups. While many natural algorithmic decision problems have been proven or are generally suspected to be undecidable for these classes, the word problem forms a notable exception. In the group case, it asks whether a given word in the generators is equal to the neutral element in the group in question and is well-known to be decidable for automaton groups. In fact, it was observed in a work by Steinberg published in 2015 that it can be solved in nondeterministic linear space using a straight-forward guess and check algorithm. In the same work, he conjectured that there is an automaton group with a PSPACE-complete word problem.

In a recent paper presented at STACS 2020, Armin Weiß and I could prove that there indeed is such an automaton group. To achieve this, we combined two ideas. The first one is a construction introduced by Daniele D'Angeli, Emanuele Rodaro and me to show that there is an inverse automaton semigroup with a PSPACE-complete word problem and the second one is an idea already used by Barrington in 1989 to encode NC¹ circuits in the group of even permutation over five elements. In the talk, we will discuss how Barrington's idea can be applied in the context of automaton groups, which will allow us to prove that the uniform word problem for automaton groups (were the generating automaton and, thus, the group is part of the input) is PSPACE- complete. Afterwards, we will also discuss the ideas underlying the construction to simulate a PSPACE-machine with an invertible automaton, which allow for extending the result to the non-uniform case. Finally, we will briefly look at related problems such as the compressed word problem for automaton groups.

Joint work with Salomon Sickert

In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of LTL with past operators is equivalent to a formula of the form $\bigwedge_{i=1}^n \G\F \varphi_i \vee \F\G \psi_i $, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for the future fragment of LTL. Both normalisation procedures had a non-elementary worst-case blow-up, and followed an involved path from LTL formulas to counter-free automata to star-free regular expressions and back to LTL. We improve on both points. We present a purely syntactic normalisation procedure from LTL to LTL, with single exponential blow-up, that can be implemented in a few dozen lines of Standard ML code. As an application, we derive a simple algorithm to translate LTL into deterministic Rabin automata. The algorithm normalises the formula, translates it into a special very weak alternating automaton, and applies a simple determinisation procedure, valid only for these special automata.

An assume guarantee (AG) specification is of the form “Assumption implies Guarantee”. AG Synthesis is the following problem: given an AG specification, construct a system satisfying it.

In this talk I will discuss the case where both Assumptions and Guarantees are given by Prompt Linear Temporal Logic (Prompt LTL), which is a logic extending LTL by adding bound requirements such as “every request is answered in bounded time”.

The solution to the AG problem for Prompt LTL will be an invitation to the theory of regular cost functions.

Joint work with Bastien Maubert and Moshe Y. Vardi.

Bertrand et al. (2017) introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min- cut theorem, and of the theory of regular cost functions.

We present a new category theoretic approach to equationally axiomatizable classes of algebras. This approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. We present a generic HSP theorem and a sound and complete equational logic, which encompass numerous flavors of equational axiomizations studied in the literature. In addition, we use the generic HSP theorem as a key ingredient to obtain Eilenberg-type correspondences yielding algebraic characterizations of properties of regular machine behaviours. When instantiated for orbit-finite nominal monoids, the generic HSP theorem yields a crucial step for the proof of the first Eilenberg-type variety theorem for data languages.

We propose a generic framework for learning unknown formal languages of various types (e.g. finite or infinite words, weighted and nominal languages). Our approach is parametric in a monad T that represents the given type of languages and their recognizing algebraic structures. Using the concept of an automata presentation of T-algebras, we demonstrate that the task of learning a T-recognizable language can be reduced to learning an abstract form of algebraic automaton whose transitions are modeled by a functor. For the important case of adjoint automata, we devise a learning algorithm generalizing Angluin’s L*. The algorithm is phrased in terms of categorically described extension steps; we provide for a termination and complexity analysis based on a dedicated notion of finiteness. Our framework applies to structures like ω-regular languages that were not within the scope of existing categorical accounts of automata learning. In addition, it yields new generic learning algorithms for several types of languages for which no such algorithms were previously known at all, including nominal languages with name binding, and cost functions. This talk is based on joint work with Lutz Schröder.

In this talk, we consider multiplayer games on graphs. In such games, each player has his own objective, that does not necessarily clash with the objectives of the other players. In this “non zero-sum” context, equilibria are a better suited solution concept than the classical winning strategy notion. We will focus on a refinement of the well-known Nash Equilibrium concept: Subgame Perfect Equilibrium (SPE for short), where players have to play rationnally in every scenario, even the ones that deviate from the planned outcome. We will explain why this refinement is a relevant solution concept in multiplayer games and show how to handle them in quantitative reachability games, where each player wants to minimize the number of steps to reach its own target set of vertices.

We consider extensions of monadic second order logic over $\omega$-words, which are obtained by adding one language that is not $\omega$-regular. We show that if the added language $L$ has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the $\omega$-regular languages are the only decidable Boolean-closed full trio over $\omega$-words.

(Joint work with Mikołaj Bojańczyk, Edon Kelmendi, and Rafał Stefański)

Transducers extend automata by adding outputs to the transition, thus computing functions over words instead of recognizing languages. Deterministic two-way transducers define the robust class of regular functions which is, among other good properties, closed under composition. However, the best known algorithms for composing two-way transducers are rather involved and cause a double exponential blow-up in the size of the input machines. This contrasts with the rather direct and polynomial construction for composing one-way machines. In this talk, I will present the class of reversible transducers, which are machines that are both deterministic and co-deterministic. This class enjoys polynomial composition complexity, even in the two-way case. Although this class is not very expressive in the one-way scenario, I will show that any two-way transducer can be made reversible through a single exponential blow-up. As a consequence, the composition of two-way transducers can be done with a single exponential blow-up in the number of states, enhancing the best known algorithm from the 60s.

The window mechanism was introduced by Chatterjee et al. to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields.

In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.

Joint work with : Thomas Brihaye, Florent Delgrange, Mickael Randour.

We study networks of processes which all execute the same finite-state protocol and communicate thanks to a rendez-vous mechanism. Given a protocol, we are interested in checking whether there exists a number, called a cut-off, such that in any networks with a bigger number of participants, there is an execution where all the entities end in some final states. We provide decidability and complexity results of this problem under various assumptions, such as absence/presence of a leader or symmetric/asymmetric rendez-vous.

This is a joint work with Florian Horn.

A language of finite words is star-free when it can be built from letters using Boolean operations and concatenation. A well-known theorem of Schützenberger characterizes star-free languages as those recognized by an aperiodic monoid. Another theorem of Schützenberger gives an alternate definition: these are the languages that can be built using product, union, and, in a limited way, Kleene star (but complement is now disallowed).

These definitions can be rephrased using closure operators operating on classes of languages. In this talk, we investigate these operators and generalize the results of Schützenberger. This is joint work with Thomas Place.

Parity games are central to the verification and synthesis of reactive systems: various model-checking, realisability and synthesis problems reduce to solving these games. Solving parity games – that is, deciding which player has a winning strategy – is one of the few problems known to be in both UP and co-UP yet not known to be in P. So far, the quest for a polynomial algorithm has lasted over 25 years.

In 2017 a major breakthrough occurred: parity games are solvable in quasi-polynomial time. Since then, several seemingly very distinct quasi-polynomial algorithms have been published, both by myself and others, and some of the novel ideas behind them have been applied to address other problems in automata theory.

In this talk, I will give an overview of these developments, including my own contribution to them, and the state-of-the art, with a slight automata-theoretic bias.