Henning Urbat

CSL Conference 2026 Conference Paper

Well-Founded Coalgebras Meet Kőnig's Lemma

• Henning Urbat
• Thorsten Wißmann

Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i. e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category ℂ, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ℂ and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space - in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.

Highlights Conference 2025 Conference Abstract

Algebraic Language Theory with Effects

• Henning Urbat

Highlights Conference 2023 Conference Abstract

Nominal Topology for Data Languages

• Henning Urbat

We propose a novel topological perspective on data languages recognizable by orbit-finite nominal monoids. For this purpose, we introduce pro-orbit-finite nominal topological spaces, a form of nominal topological spaces generalizing classical profinite spaces. Assuming globally bounded support sizes of the underlying nominal sets, which correspond to bounds on the number of registers of automata, pro-orbit-finite nominal topological spaces coincide with nominal Stone spaces and are shown to be dually equivalent to a suitable subcategory of nominal boolean algebras. Recognizable data languages are characterized as topologically clopen sets of pro-orbit-finite words. In addition, we explore the expressive power of pro-orbit-finite equations and provide a nominal version of Reiterman’s pseudovariety theorem. This talk is based on joint work with Fabian Birkmann and Stefan Milius, presented at ICALP 2023. Contributed talk given by Henning Urbat Coffee Break Thursday 16h00 - 17h00, Special Session | HS 3 | "Open Problems Tools and Experiments" Friday Friday 09h00 - 10h00, Keynote Speaker | HS 3 | chair: Slawek Lasota | Meena Mahajan - Quantified Boolean Formulas and Proof Complexity For several years, both proof complexity and practical solving focussed on propositional proof systems and detecting (un)satisfiability. In the last two decades, several proof systems for the more succinct Quantified Boolean Formulas QBFs have been proposed and studied, and several QBF solvers have been developed. This talk will give an overview of what has been achieved in QBF proof complexity, and how (if at all) it informs QBF solving. Coffee Break Friday 10h30 - 11h42, Contributed Talks Probabilistic and Timed Systems | HS 3 | chair: Michael Cadilhac Games 3 | HS 4 | chair: Maximilian P. Weininger Probabilistic and Timed Systems | HS 3 | chair: Michael Cadilhac Games 3 | HS 4 | chair: Maximilian P. Weininger

MFCS Conference 2023 Conference Paper

Positive Data Languages

• Florian Frank 0002
• Stefan Milius
• Henning Urbat

Positive data languages are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions about equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages recognizable by nondeterministic orbit-finite nominal automata, an abstract form of register automata introduced by Bojańczyk, Klin, and Lasota. As our main contribution we provide a number of equivalent characterizations of that class in terms of positive register automata, monadic second-order logic with positive equality tests, and finitely presentable nondeterministic automata in the categories of nominal renaming sets and of presheaves over finite sets.

FSCD Conference 2022 Conference Paper

Stateful Structural Operational Semantics

• Sergey Goncharov 0001
• Stefan Milius
• Lutz Schröder
• Stelios Tsampas 0001
• Henning Urbat

Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.

MFCS Conference 2021 Conference Paper

Syntactic Minimization Of Nondeterministic Finite Automata

• Robert S. R. Myers
• Henning Urbat

Nondeterministic automata may be viewed as succinct programs implementing deterministic automata, i. e. complete specifications. Converting a given deterministic automaton into a small nondeterministic one is known to be computationally very hard; in fact, the ensuing decision problem is PSPACE-complete. This paper stands in stark contrast to the status quo. We restrict attention to subatomic nondeterministic automata, whose individual states accept unions of syntactic congruence classes. They are general enough to cover almost all structural results concerning nondeterministic state-minimality. We prove that converting a monoid recognizing a regular language into a small subatomic acceptor corresponds to an NP-complete problem. The NP certificates are solutions of simple equations involving relations over the syntactic monoid. We also consider the subclass of atomic nondeterministic automata introduced by Brzozowski and Tamm. Given a deterministic automaton and another one for the reversed language, computing small atomic acceptors is shown to be NP-complete with analogous certificates. Our complexity results emerge from an algebraic characterization of (sub)atomic acceptors in terms of deterministic automata with semilattice structure, combined with an equivalence of categories leading to succinct representations.

Highlights Conference 2018 Conference Abstract

Eilenberg Theorems for Free

• Henning Urbat

ABSTRACT. Algebraic language theory investigates the behaviors of finite machines by relating them to finite algebraic structures. For instance, regular languages - the behaviours of finite automata - can be described purely algebraically as the languages recognized by finite monoids, and a fundamental relation between these concepts is given by Eilenberg’s variety theorem: varieties of languages (classes of regular languages closed under boolean operations, derivatives, and preimages of monoid morphisms) correspond bijectively to pseudovarieties of monoids (classes of finite monoids closed under homomorphic images, submonoids, and finite products). This together with Reiterman's theorem, which characterizes pseudovarieties as the classes of monoids presentable by profinite equations, establishes a firm connection between automata, algebra, topology, and logic. Dozens of extensions of these results are known which consider either notions of varieties with modified closure properties, or other types languages such as omega-regular languages, tree languages or cost functions. In this talk, I will outline a uniform category theoretic approach to algebraic language theory that encompasses all the above work. The key idea is to (1) model languages and the algebraic structures recognizing them by a monad T on some algebraic category D; (2) interpret profinite equations and Reiterman’s theorem by means of a codensity monad induced by T, called the profinite monad; and (3) interpret the algebraic recognition of languages in terms of second algebraic category C that dualizes to D on the level of finite algebras. As a result, we obtain an Eilenberg-Reiterman correspondence which establishes a bijective correspondence between varieties of T-recognizable languages, pseudovarieties of T-algebras, and profinite equational theories. The classical case of regular languages is recovered by taking the categories C = boolean algebras and D = sets, and the free-monoid monad on D. Likewise, by varying the parameters, almost all Eilenberg-Reiterman correspondences known in the literature emerge as special cases of the categorical framework. In addition, a number of new results come for free, including a variety theorem for data languages. The presentation is based on the recent paper: H. Urbat, J. Adámek, L. -T. Chen, S. Milius: Eilenberg Theorems for Free. Proc. 42nd International Symposium on Mathematical Foundations of Computer Science (2017). EATCS Best Paper Award. LIPIcs, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

MFCS Conference 2017 Conference Paper

Eilenberg Theorems for Free

• Henning Urbat
• Jirí Adámek
• Liang-Ting Chen 0001
• Stefan Milius

Eilenberg-type correspondences, relating varieties of languages (e. g. , of finite words, infinite words, or trees) to pseudovarieties of finite algebras, form the backbone of algebraic language theory. We show that they all arise from the same recipe: one models languages and the algebras recognizing them by monads on an algebraic category, and applies a Stone-type duality. Our main contribution is a variety theorem that covers e. g. Wilke's and Pin's work on infinity-languages, the variety theorem for cost functions of Daviaud, Kuperberg, and Pin, and unifies the two categorical approaches of Bojanczyk and of Adamek et al. In addition we derive new results, such as an extension of the local variety theorem of Gehrke, Grigorieff, and Pin from finite to infinite words.

TCS Journal 2015 Journal Article

Coalgebraic constructions of canonical nondeterministic automata

• Robert S.R. Myers
• Jiří Adámek
• Stefan Milius
• Henning Urbat

For each regular language L we describe a family of canonical nondeterministic acceptors (nfas). Their construction follows a uniform recipe: build the minimal dfa for L in a locally finite variety V, and apply an equivalence between the category of finite V -algebras and a suitable category of finite structured sets and relations. By instantiating this to different varieties, we recover three well-studied canonical nfas: V = boolean algebras yields the átomaton of Brzozowski and Tamm, V = semilattices yields the jiromaton of Denis, Lemay and Terlutte, and V = Z 2 -vector spaces yields the minimal xor automaton of Vuillemin and Gama. Moreover, we obtain a new canonical nfa called the distromaton by taking V = distributive lattices. Each of these nfas is shown to be minimal relative to a suitable measure, and we derive sufficient conditions for their state-minimality. Our approach is coalgebraic, exhibiting additional structure and universal properties of the canonical nfas.