Categories for Automata and Language Theory

In this talk I would like to discuss the connection between algebra (e.g. semigroups) and logic (e.g. $\mathrm{MSO}$) for defining languages, in a categorical perspective, which is meant to be helpful for generalisations beyond words.There are in fact two perspectives: one, using monads, focuses on algebras, and logic becomes a derived notion. This talk is about a dual perspective, where logic is the basic notion, and algebras are derived. The main topic of interest is $\mathrm{MSO}$-transductions.

This tutorial introduced string diagrams, a mathematical notation that originates in (monoidal) category theory, through a computer science lens. In particular, the focus was on string diagrams *as syntax*, generalising classical syntax. Because string diagrams do not have an implicit assumption on the classicality of the underlying data, they are particularly useful for resource sensitive applications. After some discussion of the notion of monoidal theory, generalising the classical notion of algebraic theory, the tutorial finished with the notion of monoidal automaton (joint work with Matt Earnshaw) that accepts languages of string diagrams.

In this tutorial I gave an introduction to universal coalgebra as a general categorical framework for state-based evolving systems. After presenting some motivating examples I formally introduced coalgebras for a set functor T, as well as their morphisms. I then discussed final coalgebras and the concept of coinduction, as a principle for giving both definitions and proofs. I finished with discussing the notions of behavioral equivalence and bisimilarity, and their relationship.

The talk gave an introduction to some fibrational concepts from category theory and the relevance to studying “lifting problems” in logic, automata, and language theory. After presenting some general ideas on representing deductive systems as “bundles of categories”, the bulk of the talk focused on finite-state automata, starting from the classical idea of representing the transition graph of an NFA by a graph homomorphism $\varphi :G\to B_{\mathrm{\Sigma }}$ into the bouquet graph with set of loops $\mathrm{\Sigma }$, and considering the corresponding functor $p=F\varphi :FG\to F{B}_{\mathrm{\Sigma }}$ between free categories. We discussed how to characterize determinism and codeterminism: $\varphi$ represents the transition graph of a complete DFA (respectively coDFA) just in case $p$ is a discrete opfibration (respectively discrete fibration). Next, emphasizing the importance of the general case, we showed how to characterize functors representing arbitrary (potentially ambiguous) nondeterministic finite-state automata: a functor $p:D\to F{B}_{\mathrm{\Sigma }}$ represents an NFA just in case $p$ satisfies the unique lifting of factorizations (ULF) and finitary fiber properties. Finally, we explained how to use this characterization to define NFA over arbitrary categories, recognizing regular languages of arrows.

The tutorial was based on joint work with Paul-André Melliès.

We study automata weighted over number rings, that is, rings of integers in an algebraic number field.

We show that number rings are what we call “almost strong Fatou”: if an n-state automaton weighted in a number field recognizes an integer-valued series, then it admits an equivalent n+1-state automaton weighted in the corresponding ring of integers.

We then explain how this fits in a bigger categorical picture: given a well-behaved functor F, we give a generic procedure for retrieving the minimal C-automaton from any D-automaton. This gives in particular a generic reduction of the problem of actively learning C-automata to the problem of actively learning D-automata, which instantiates in particular to a reduction from actively learning automata weighted in number rings to automata weighted in number fields.

A monad-based denotational model is introduced, which is shown to be adequate for the Proto-Quipper family of calculi, themselves being idealized versions of the Quipper programming language. The use of a monadic approach allows us to keep the value to which a term reduces distinct from the circuit that the term itself produces as a side-effect. In turn, this enables the denotational interpretation of rich type systems in which even the size of the produced circuit is controlled, at the same time justifying some of the design novelties present in such calculi.

The talk introduces effectful Mealy machines and gives them semantics both in terms of bisimilarity and traces. Bisimilarity is characterised syntactically, via free uniform feedback. Traces are a coinductive construction. Effectful Mealy machines, their bisimilarity and trace capture existing flavours of Mealy machines, bisimilarity and trace.

We introduce context-free languages of morphisms in monoidal categories, extending recent work on the categorification of context-free languages, and regular languages of string diagrams. Context-free languages of string diagrams include classical context-free languages of words, trees, and hypergraphs, when instantiated over appropriate monoidal categories. We prove a representation theorem for context-free languages of string diagrams: every such language arises as the image under a monoidal functor of a regular language of string diagrams.

We introduce higher-dimensional automata (HDAs) and their languages, which consist of interval pomsets with interfaces (ipomsets). We then show a decomposition property which allows to develop an isomorphism between the category of ipomsets and a category generated by special discrete ipomsets (“starters” and “terminators”) under the relation which allows to compose subsequent starters and subsequent terminators. This in turn allows us to introduce an operational semantics for HDAs as so-called ST-automata: finite automata over the graph alphabet of starters and terminators.

Fixpoints play an important role in both denotational semantics where they are used to represent recursively defined programs and data types as well as in operational semantics where many behavioral equivalences are obtained as fixpoints of some relation transformers.

In the categorical theory of fixpoint operators, we usually consider one fixpoint operator at a time and little attention is given to the study of mixed fixpoint operators where we take a different fixpoint operator for each variable. Systems combining least and greatest fixpoints over lattices are an important example as they are the basis of many static analysis and model checking methods.

I will present in this talk an axiomatization of mixed fixpoint operators first in the 1-categorical setting and then briefly mention how to extend to 2-categories in order to capture the examples of initial algebras and coalgebras of accessible functors, analytic and polynomial functors.

F-coalgebra automata provide a unifying, categorical setting for studying automata-theoretic verification of a variety of system types. For certain applications in quantitative model checking [1], it is crucial that the property to be checked is given by an unambiguous automaton, i.e., there is at most one accepting run on each input. This leads to the question of when unambiguous F-coalgebra automata exist. This question is also of fundamental interest, beyond verification.

For infinite words, the situation is easy, since parity word automata can be determinised. For trees, it is known that deterministic automata are less expressive than nondeterministic ones, but one can recover unambiguous acceptance when restricting to thin trees, i.e., trees with only countably many infinite branches [2, 3].

Inspired by the results on thin trees, we aim to develop a similar theory for thin F-coalgebras. This talk presents the first part of this program. We show that for analytic functors F, we can define thin F-coalgebras as those coalgebras with only countably many infinite paths from each state. Our main result is an inductive characterisation of thinness via an initial algebra. To this end, we develop a syntax for thin behaviours and give a sound and complete axiomatisation of when two terms represent the same thin behaviour. Finally, for the special case of polynomial functors (the type of ranked ordered trees), we retrieve from our syntax the notion of Cantor-Bendixson rank of a thin tree.

Regular languages – the languages accepted by deterministic finite automata – are known to be precisely the languages recognized by finite monoids. This characterization is the origin of algebraic language theory. We generalize the correspondence between automata and monoids to automata with generic computational effects given by a monad, providing the foundations of an effectful algebraic language theory. We show that, under suitable conditions on the monad, a language is accepted by an effectful finite automaton precisely when it is recognizable by (1) an effectful monoid morphism into an effect-free finite monoid, and (2) a monoid morphism into a monad-monoid bialgebra whose carrier is a finitely generated algebra for the monad, the former mode of recognition being conceptually completely new. As applications we obtain novel algebraic characterizations of probabilistic finite automata, nondeterministic probabilistic finite automata, and for weighted finite automata over unrestricted semirings, generalizing previous work on weighted algebraic recognition over commutative rings.

We enrich the functorial viewpoint on automata of Colcombet and Petrişan to work with automata in any topos. The whole minimisation framework adapts to enrichment with notably enriched Kan extensions and enriched orthogonal factorisation systems. We use this general minimisation to deduce a general Myhill-Nerode theorem. This theorem depends on a notion of “finiteness”. By instantiating this framework with the topos of nominal sets and the orbit-finiteness, we recover the Myhill-Nerode theorem of Bojańczyk, Klin and Lasota. But the theorem applies to other finiteness conditions, such as Kuratowski-finiteness or “stalkwise-finiteness”. Moreover, the whole enriched framework can work with other monoidal categories than toposes.

We generalize Courcelle’s recognizable graph languages and results on monadic second-order logic to more general structures.

We give a category-theoretical characterization of recognizability. A recognizable subset of arrows in a category is defined via a functor into the category of relations on finite sets. This can be seen as a straightforward generalization of finite automata and we show how to obtain graph automata - accepting recognizable graph languages – by applying the theory to the category of cospans of graphs.

We also introduce a simple logic that allows to quantify over the subobjects of a categorical object and we show that, for the category of graphs, this logic is equally expressive as monadic second-order graph logic (MSOGL). Furthermore, we explain that in the more general setting of hereditary pushout categories, a class of categories closely related to adhesive categories, we can recover Courcelle’s result that every MSOGL-expressible property is recognizable.

The talk concludes by reviewing a practical implementation of graph automata with applications to the verification of graph transformation systems.

In this talk, I explained how to establish a “run-aware” version of the Myhill-Nerode theorem based on a fibrational / categorical account of Brzozowski derivatives. A non-deterministic finite state automaton is defined as a finitary functor $p:E\to B$ satisfying the unique lifting of factorisation (ULF) property, where E is a category of states and runs, and B is a category of sorts and words.

A relative family construction is introduced, which provides a “categorified” powerset construction for any functor $p:E\to B$. One key observation is that the resulting functor $\mathrm{Fam}(E,p)\to B$ is a fibration if and only if $p$ is a ULF functor.

The observation is applied to the finitary and ULF functor $p^{\mathrm{op}}\times p:E^{\mathrm{op}}\times E\to B^{\mathrm{op}}\times B$ in order to obtain a fibration $\mathrm{Fam}(E^{\mathrm{op}}\times E,p^{\mathrm{op}}\times p)\to B^{\mathrm{op}}\times B$ together with a functor $F^{†}:\mathrm{Fam}(E^{\mathrm{op}}\times E,p^{\mathrm{op}}\times p)\to {\mathrm{Lang}}^{\to }$ over $B^{\mathrm{op}}\times B$ where the fibration ${\mathrm{Lang}}^{\to }\to B^{\mathrm{op}}\times B$ is the pullback of the codomain fibration ${\mathrm{Set}}^{\to }\to \mathrm{Set}$ along the hom functor ${\mathrm{hom}}_B:B^{\mathrm{op}}\times B\to \mathrm{Set}$. The functor $F^{†}$ itself is obtained from the functor ${\mathrm{hom}}_p:E^{\mathrm{op}}\times E\to {\mathrm{Set}}^{\to }$ which transports every pair of states $(R,S)$ to the function ${\mathrm{Hom}}_p:{\mathrm{Hom}}_E(R,S)\to {\mathrm{Hom}}_B(A=pR,B=pS)$ associated to the functor $p$.

The functor $F^{†}$ is shown to transport cartesian maps to cartesian maps in ${\mathrm{Lang}}^{\to }\to B^{\mathrm{op}}\times B$ which appear as a “run-aware” form of Brzozowski derivatives in $Lan{g}^{\to }$. From this follows a Myhill-Nerode theorem for “run-aware” languages, stating that a language $L$ is regular if and only if its class of derivatives is finitely generated (using sums or disjoint unions) at each fiber over an object of the category $B^{\mathrm{op}}\times B$.

Regular languages – the languages accepted by deterministic finite automata – are known to be precisely the languages recognized by finite monoids. This characterization is the origin of algebraic language theory. We generalize the correspondence between automata and monoids to probabilistic automata, providing the foundations of a probabilistic algebraic language theory. We show that a language is computable by a probabilistic finite automaton precisely when it is recognizable by (1) a probabilistic monoid morphism into an (ordinary) finite monoid, and (2) an (ordinary) monoid morphism into an fg-carried convex monoid: a finitely generated convex set equipped with a monoid operation that distributes over the convex structure. The former mode of recognition is conceptually completely new. Moreover, every probabilistic laguage has a syntactic monoid, that is, a minimal algebraic recognizer. However, the syntactic monoid is not fg-carried in general. As an open problem we leave the question whether the syntactiv monoid is finitely presentable as a convex monoid.

A fundamental observation at the heart of the topological approach to language theory is the fact that the topological space of profinite words is the Stone dual of the Boolean algebra of regular languages Reg($\mathrm{\Sigma }$) over the alphabet $\mathrm{\Sigma }$. Using ideas coming from the seminal work of Salvati on languages of $\lambda$-terms, who introduced the family of Boolean algebras Reg(A) for any type A, we introduce the space of profinite $\lambda$-terms of type A as the Stone dual of Reg(A), which generalizes to the higher-order setting the notion of profinite word. Types and profinite $\lambda$-terms assemble into a Stone-enriched cartesian closed category ProLam, which is the free such category C that recognizes at most regular languages in the sense of Salvati. This demonstrates the compositional aspects of profinite $\lambda$-terms, which we think of as the terms of an extension of the $\lambda$-calculus with profinite operators.

Given a regular language Omega and a class of regular languages V, we want to understand when the class of languages that can be written as the intersection of Omega with a a language from V has decidable membership. We provide a sufficient condition on Omega such that whenever V has decidable membership (and has some mild closure properties, i.e. is a pseudovariety), then the relativization of V with respect to Omega also has decidable membership.

In the last decade or so, higher-order recursion schemes (HORS) have emerged as a promising technique for model-checking higher-order programs. I will discuss several results concerning the case when HORS are typed using linear logic (intuitionistic multiplicative additive linear logic, to be precise). It turns out that such schemes have an automata-theoretic counterpart, namely restricted tree-stack automata, which come from linguistics, where they were introduced to study the so-called multiple context-free languages. This leads to a new perspective on linear HORS and new decidability results. This is joint work with Pierre Clairambault (deterministic case, MFCS’19), Guanyan Li and Luke Ong (probabilistic case, LICS’22).

A string-to-string function is regular (i.e. is an $\mathrm{MSO}$-transduction) if and only if it factors as

where $F$ is a finiteness-preserving endofunctor on semigroups, and ${\mathrm{out}}_{{\mathrm{\Gamma }}^{\ast }}$ is a component of a natural transformation

In the talk, I have provided a new categorical perspective on the algebraic approach to the constraint satisfaction problem (CSP). The approach has been a prevalent method of the study of the complexity of these problems since the early 2000s, and many breakthrough achievements can be either directly or indirectly attributed to it. A prime result is the Bulatov–Zhuk Dichotomy Theorem, which states that every finite-template CSP is either in P or NP-complete.

I have explained the gadget reductions used by the algebraic approach as a case of a well-known categorical construction (left Kan extension along Yoneda), and I have stated and proved the fundamental theorem of the algebraic approach in the categorical language. The theorem provides a condition for a CSP to be NP-complete that covers the hardness part of the dichotomy.

In this talk I present a categorical approach to automata based on the categorical notion of functor. The basic idea is to see an automaton as a machine taking some input specified by an “input” category and producing some effect – such as non-determinism, words over an output alphabet or probability values – encoded by an “output” category. Usually, the output category is a Kleisli category for a monad specifying a given effect. We discuss how adjunctions between categories can be lifted to adjunctions between categories of automata, encompassing examples such as determinization or completion. We then present sufficient conditions on the output category such that minimization and learning algorithms exist.

Weihrauch reducibility is a notion that has gained a lot of traction in computable analysis in the last decade. It may be regarded as a framework to compare the uncomputational strength of problems, much like reverse mathematics.

Weihrauch problems include natural mathematical problems such as WKL and RT, but the corresponding degrees also enjoy a rich algebraic structure induced by algebraic operation on problems. A great number of these operations correspond to the structure of the category problems and reductions, which is equivalent to (a full subcategory of) the category of containers/polynomials over represented spaces and computable maps, a well-known nice category which is bicartesian closed and monoidal closed among other things.

After introducing these notions, I will discuss the equational theory of the Weihrauch lattice equipped with the composition product and finite iterations thereof. Terms in this theory can be translated to alternating automata, and reductions regarded as a somewhat weird kind of simulation. This leads to decidability and a complete axiomatization.

Very little to the development is specific to Weihrauch problems and could potentially be adapted to handle containers over a range of extensive locally cartesian closed categories with dependent W-types.

Conformance testing is often used to implement the equivalence query in active automata learning. In this talk, I will highlight this application, and go on to discuss the basic notions of $n$-completeness and the classical $W$-method. I will then discuss recent joint work with Bálint Kocsis ([1], to appear at FoSSaCS 2025) on generalising part of this theory to the abstract setting of automata in a category.

A language L is said to be regular measurable if there exists an infinite sequence of regular languages that “converges” to L. This notion was introduced by the speaker in 2021 [1] and used for classifying non-regular languages by using regular languages. In this talk, we describe why this notion was introduced, and give a brief overview of decidability results relating to the measurability on subclasses (local subvarieties) of regular languages, eg., star-free, generalised definite, and group languages.

Formal languages over infinite alphabets serve the modelling and specification of structures and processes with data; here, infinite alphabets represent infinite data types equipped with very restricted interfaces, typically just checks for (in)equality. Such formal languages are thus typically referred to as data languages. There is a large variety of automata models for data languages; one of the most established models is the classical register automaton model, in which letters encountered in the input can be stored in a fixed number of registers for later comparison with other letters. Register automata are generally equivalent to automata models over nominal sets; for instance, nondeterministic register automata with nondeterministic update are equivalent to nondeterministic orbit-finite automata. In such equivalences, states of a nominal automaton correspond to configurations of a register automaton, consisting of a control state and the current register content.

In register-based models, expressiveness typically varies with the power of control; e.g., nondeterministic register automata are strictly more expressive than deterministic ones. While membership is typically decidable, inclusion of register automata tends to be either undecidable or of prohibitively high complexity unless stringent restrictions are imposed on either the power of control, e.g. requiring unambiguity, or on the number of registers. We introduce nominal automata models with explicit name allocation, which strike a compromise between expressive power and complexity. In such models, freshness of letters is modelled via alpha-equivalence on words with explicit allocation. Roughly speaking, this means that distinctness of a newly read letter with respect to a stored letter can only be enforced if the stored letter is expected to be seen again. This still allows for typical modes of expression requiring, for instance, explicit closure of named sessions; on the other hand, it allows for inclusion checking in elementary time under unrestricted nondeterminism and without bounding the number of registers. Indeed, the complexity is typically no worse than the complexity of the corresponding finite-alphabet model when the number of registers is fixed as a parameter. This has originally been established for non-deterministic finite-word automata with name allocation; similar results have subsequently been obtained for infinite-word automata, tree automata, and, very recently, for alternating finite-word automata.

In 1967, Lovász showed that two graphs $G$ and $H$ are isomorphic if, and only if, they admit the same number of homomorphisms from every graph $F$. Subsequently, it emerged that many natural graph isomorphism relaxations from fields as diverse as finite model theory, category theory, optimization, quantum information, and algebraic graph theory can be characterized as homomorphism indistinguishability relations over natural restricted graph classes.

In this talk, we set out to abstract from these examples and develop a theory of homomorphism indistinguishability. We propose to answer, given a graph class $ℱ$, the following questions:

1. 1.

   What is the distinguishing power of the homomorphism indistinguishability relation ${\equiv }_{ℱ}$ of $ℱ$?

2. 2.

   What is the complexity of deciding homomorphism indistinguishability over $ℱ$?

We discuss progress on both questions covering Roberson’s conjecture on the homomorphism distinguishing closure, a recent result of myself on the complexity of homomorphism indistinguishability over recognizable $ℱ$ of bounded treewidth, and the role of minor-closed graph classes in the emerging theory of homomorphism indistinguishability.

Model-comparison games are an important tool in both finite and unrestricted model theory to prove when two structures satisfy the same sentences in a logic. Game comonads encode particular model comparison games as comonads on the categories of structures. This started with the work of Abramsky, Dawar, and Wang in 2017 on encoding pebble games for finite variable logics. Since this initial work, several examples of have comonads have been engineered to capture a wide-range of logics. Each game comonad provides a categorical characterisation of equivalence in a logic and its variants. The categorical constructions common to these comonads have proved to be a nice tool for organizing tacit connections between syntactic resources in logic, hierarchical approximations to constraint satisfaction and isomorphism, and well-known combinatorial parameters such as treewidth and tree-depth.

Determining the commonalities shared amongst game comonads that enable them to have these features lead to the axiomatic formulation of arboreal category and arboreal cover by Abramsky and Reggio 2021. Arboreal categories axiomatise the notion of a category with “tree-shaped” objects and provide a native setting for dynamic notions like simulation, bisimulation, and resource-indexing. Arboreal covers are comonadic adjunctions to any category that allow application of these dynamic notions to the static objects of the target category. Game comonads all arise as arboreal covers over categories of relational structures.

We shall connect classical algebraic model theory with monadic second order logic (MSOL) on infinite structures (natural numbers, infinite binary trees, infinite trees of arbitrary degrees, etc.)

The idea comes from the well-known connection between MSOL and automata: this connection allows a conversion between MSOL formulae and suitable automata (and back). Applying such conversion, every MSOL formula turns out to be equivalent to a formula which is “almost existential”. The “almost” proviso (coming from acceptation conditions) can be removed if the language is enriched with some temporal operators in LTL/CTL style.

First-order theories whose formulae are equivalent to existential formulae are precisely model complete theories. MSOL interpreted on a structure can be viewed as first-order logic (FOL) interpreted on the corresponding power set Boolean first-order structures. From these facts we may formulate the slogan “MSOL is the model companion of temporal logic”. The aim of the talk is to supply results giving a precise formal meaning to such slogan.

This talk is about recent results on axiomatizing infinite trace semantics, also called stream semantics, for generative probabilistic transition systems, also called labelled Markov chains.

The talk is about trace semantics and its equational (sound and complete) axiomatization. Probabilistic transition systems can be represented by suitable probabilistic expressions, with the property that the expression and the transition system (state) have the same (in this case trace) semantics. We then provide equations on these expressions that fully characterize (infinite) trace semantics: two expressions are trace equivalent iff they are provably equivalent with the presented axioms. The axioms for finite traces have been given by Silva and myself in 2011. The soundness and completeness proof is coalgebraic.

In recent work with the group of coathors mentioned above, we present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets - in particular on a novel and simpler proof of properness of the involved functor. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.

In this work with Amina Doumane and Denis Kuperberg, we establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal $\mu$-calculus, a question that had remained open for several decades. The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognised by finitary tree algebras whose sorts zero and one are finite are the regular ones. This corresponds for trees to a weak form of the key translation of Wilke algebras to $\omega$-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years.

In this talk, we show how profinite words are types, in the model-theoretic sense, for monadic second-order logic. Starting from the Stone duality approach to regular languages developed in [1], we show how the free profinite monoid naturally arises as the dual of a colimit chain of finite Boolean algebras with operators. In the first-order setting, this leads to the model-theoretic view on proaperiodic monoids developed in [2]. We also mention links with the duality-theoretic notion of preserving joins at primes [3, Ch. 8]. These considerations were generalized to give profinite lambda-terms in [4], also see V. Moreau’s talk in the same seminar.

The Janin-Walukiewicz Theorem states that on Kripke models, the modal $\mu$-calculus is the bisimulation-invariant fragment of monadic second-order logic. In the talk I showed how to generalise this result to T-coalgebras for an arbitrary set functor T (satisfying some conditions). In the proof I introduced the notion of coalgebra automata.

I introduce presheaf automata as presheaves over categories with two distinguished families of morphisms. Presheaf automata are a generalisation of different variants of higher-dimensional automata and other automata-like formalisms, including Petri nets and pushdown automata. I develop the foundations of a language theory for them and define runs, languages, notions of regularity and rationality of languages, determinism and bisimulations.