arXiv subjects

Thorsten Wißmann

Publications and source records attributed to Thorsten Wißmann.

At least 19 recordsLinked to original sources

arXiv2026

Formalized Run-Time Analysis of Active Learning -- Coalgebraically in Agda

The objective of automata learning is to reconstruct the implementation of a hidden automaton, to which only a teacher has access. The learner can ask certain kinds of queries to the teacher to gain more knowledge about the hidden automaton. The run-time of such a learning algorithm is then measured in the number of queries it takes until the hidden automaton is successfully reconstructed, which is usually parametric in the number of states of that hidden automaton. How can we prove such a run-time complexity of learning algorithms in a proof assistant if we do not have the hidden automaton and the number of states available? In the present paper, we solve this by considering learning algorithms themselves as generalized automata, more specifically as coalgebras. We introduce formal and yet compact definitions of what a learner and a teacher are, which make it easy to prove upper and lower bounds of different kinds of learning games in the proof assistant Agda. As a running example, we discuss the common number guessing game where a teacher thinks of a natural number and answers guesses by the learner with `correct', `too high', or `too low'. To demonstrate our framework, we formally prove in Agda that binary search finds the teacher's secret number $n$ within $\mathcal{O}(\log n)$ guesses and that no learning strategy can guarantee fewer than $\log_2(n)$ guesses. We apply our framework to automata learning to prove the following complexity bounds in Agda: (1) If the teacher does not provide counterexamples, then there is no learning algorithm that uses only polynomially many queries. (2) The $L^{\#}$-learning algorithm takes $\mathcal{O}(k\cdot n^2 + n\cdot \log(m))$ queries to learn a Mealy machine with $k$ input symbols, $n$ states, where $m$ is the maximum length of the teacher's counterexamples.

cs.FL↗

arXiv2025

Intrinsically Correct Algorithms and Recursive Coalgebras

Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, the correctness of the corresponding algorithms follows intrinsically just from the type of the computed maps. However, proving recursivity of the underlying coalgebras is non-trivial, and proofs are typically ad hoc. This layer of complexity impedes the formalization of coalgebraically defined recursive algorithms in proof assistants. We introduce a framework for constructing coalgebras which are intrinsically recursive in the sense that the type of the coalgebra guarantees recursivity from the outset. Our approach is based on the novel concept of a well-founded functor on a category of families indexed by a well-founded relation. We show as our main result that every coalgebra for a well-founded functor is recursive, and demonstrate that well-known techniques for proving recursivity and termination such as ranking functions are subsumed by this abstract setup. We present a number of case studies, including Quicksort, the Euclidian algorithm, and CYK parsing. Both the main theoretical result and selected case studies have been formalized in Cubical Agda.

cs.PL↗

arXiv2025

Well-Founded Coalgebras Meet K\"onig's Lemma

K\"onig'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\"onig'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 C, such as the category of posets, nominal sets, or convex sets. Our coalgebraic K\"onig's lemma states that, under mild assumptions on C 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\"onig'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.

cs.LO↗

arXiv2025

Algebraic Language Theory with Effects

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. In this paper, 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 computable by an effectful 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. Our prime application is a novel algebraic approach to languages computed by probabilistic finite automata. Additionally, we derive new algebraic characterizations for nondeterministic probabilistic finite automata and for weighted finite automata over unrestricted semirings, generalizing previous results on weighted algebraic recognition over commutative rings.

cs.FL↗

arXiv2025

Trees in Coalgebra from Generalized Reachability

An automaton is called reachable if every state is reachable from the initial state. This notion has been generalized coalgebraically in two ways: first, via a universal property on pointed coalgebras, namely, that a reachable coalgebra has no proper subcoalgebras; and second, a coalgebra is reachable if it arises as the union of an iterative computation of successor states, starting from the initial state. In the current paper, we present corresponding universal properties and iterative constructions for trees. The universal property captures when a coalgebra is a tree, namely, when it has no proper tree unravellings. The iterative construction unravels an arbitrary coalgebra to a tree. We show that this yields the expected notion of tree for a variety of standard examples. We obtain our characterization of trees by first generalizing the previous theory of reachable coalgebras and of a minimal object in a category, related to projectivity. Surprisingly, both the universal property and the iterative construction for trees arise as instances of this generalized notion of reachability. Our iterative construction works for all analytic set functors.

cs.LO↗

arXiv2024

Initial Algebras Unchained -- A Novel Initial Algebra Construction Formalized in Agda

The initial algebra for an endofunctor F provides a recursion and induction scheme for data structures whose constructors are described by F. The initial-algebra construction by Adámek (1974) starts with the initial object (e.g. the empty set) and successively applies the functor until a fixed point is reached, an idea inspired by Kleene's fixed point theorem. Depending on the functor of interest, this may require transfinitely many steps indexed by ordinal numbers until termination. We provide a new initial algebra construction which is not based on an ordinal-indexed chain. Instead, our construction is loosely inspired by Pataraia's fixed point theorem and forms the colimit of all finite recursive coalgebras. This is reminiscent of the construction of the rational fixed point of an endofunctor that forms the colimit of all finite coalgebras. For our main correctness theorem, we assume the given endofunctor is accessible on a (weak form of) locally presentable category. Our proofs are constructive and fully formalized in Agda.

cs.LO↗

arXiv2023

Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence

We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time O((m+n) log n) on systems with n states and m transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was O(mn).

cs.LO↗

arXiv2023

Bisimilar States in Uncertain Structures

We provide a categorical notion called uncertain bisimilarity, which allows to reason about bisimilarity in combination with a lack of knowledge about the involved systems. Such uncertainty arises naturally in automata learning algorithms, where one investigates whether two observed behaviours come from the same internal state of a black-box system that can not be transparently inspected. We model this uncertainty as a set functor equipped with a partial order which describes possible future developments of the learning game. On such a functor, we provide a lifting-based definition of uncertain bisimilarity and verify basic properties. Beside its applications to Mealy machines, a natural model for automata learning, our framework also instantiates to an existing compatibility relation on suspension automata, which are used in model-based testing. We show that uncertain bisimilarity is a necessary but not sufficient condition for two states being implementable by the same state in the black-box system. To remedy the failure of the one direction, we characterize uncertain bisimilarity in terms of coalgebraic simulations.

cs.DM↗

arXiv2023

Action Codes

We provide a new perspective on the problem how high-level state machine models with abstract actions can be related to low-level models in which these actions are refined by sequences of concrete actions. We describe the connection between high-level and low-level actions using \emph{action codes}, a variation of the prefix codes known from coding theory. For each action code ${\mathcal{R}}$, we introduce a \emph{contraction} operator $α_{\mathcal{R}}$ that turns a low-level model $\mathcal{M}$ into a high-level model, and a \emph{refinement} operator $ρ_{\mathcal{R}}$ that transforms a high-level model $\mathcal{N}$ into a low-level model. We establish a Galois connection $ρ_{\mathcal{R}}(\mathcal{N}) \sqsubseteq \mathcal{M} \Leftrightarrow \mathcal{N} \sqsubseteq α_{\mathcal{R}}(\mathcal{M})$, where $\sqsubseteq$ is the well-known simulation preorder. For conformance, we typically want to obtain an overapproximation of model $\mathcal{M}$. To this end, we also introduce a \emph{concretization} operator $γ_{\mathcal{R}}$, which behaves like the refinement operator but adds arbitrary behavior at intermediate points, giving us a second Galois connection $α_{\mathcal{R}}(\mathcal{M}) \sqsubseteq \mathcal{N} \Leftrightarrow \mathcal{M} \sqsubseteq γ_{\mathcal{R}}(\mathcal{N})$. Action codes may be used to construct adaptors that translate between concrete and abstract actions during learning and testing of Mealy machines. If Mealy machine $\mathcal{M}$ models a black-box system then $α_{\mathcal{R}}(\mathcal{M})$ describes the behavior that can be observed by a learner/tester that interacts with this system via an adaptor derived from code ${\mathcal{R}}$. Whenever $α_{\mathcal{R}}(\mathcal{M})$ implements (or conforms to) $\mathcal{N}$, we may conclude that $\mathcal{M}$ implements (or conforms to) $γ_{\mathcal{R}} (\mathcal{N})$.

cs.FL↗

arXiv2023

Weighted and Branching Bisimilarities from Generalized Open Maps

In the open map approach to bisimilarity, the paths and their runs in a given state-based system are the first-class citizens, and bisimilarity becomes a derived notion. While open maps were successfully used to model bisimilarity in non-deterministic systems, the approach fails to describe quantitative system equivalences such as probabilistic bisimilarity. In the present work, we see that this is indeed impossible and we thus generalize the notion of open maps to also accommodate weighted and probabilistic bisimilarity. Also, extending the notions of strong path and path bisimulations into this new framework, we show that branching bisimilarity can be captured by this extended theory and that it can be viewed as the history preserving restriction of weak bisimilarity.

cs.LO↗

arXiv2022

Fast Coalgebraic Bisimilarity Minimization

Coalgebraic bisimilarity minimization generalizes classical automaton minimization to a large class of automata whose transition structure is specified by a functor, subsuming strong, weighted, and probabilistic bisimilarity. This offers the enticing possibility of turning bisimilarity minimization into an off-the-shelf technology, without having to develop a new algorithm for each new type of automaton. Unfortunately, there is no existing algorithm that is fully general, efficient, and able to handle large systems. We present a generic algorithm that minimizes coalgebras over an arbitrary functor in the category of sets as long as the action on morphisms is sufficiently computable. The functor makes at most $\mathcal{O}(m \log n)$ calls to the functor-specific action, where $n$ is the number of states and $m$ is the number of transitions in the coalgebra. While more specialized algorithms can be asymptotically faster than our algorithm (usually by a factor of $\mathcal{O}(\frac{m}{n})$), our algorithm is especially well suited to efficient implementation, and our tool Boa often uses much less time and memory on existing benchmarks, and can handle larger automata, despite being more generic.

cs.FL↗

arXiv2022

Coalgebra Encoding for Efficient Minimization

Recently, we have developed an efficient generic partition refinement algorithm, which computes behavioural equivalence on a state-based system given as an encoded coalgebra, and implemented it in the tool CoPaR. Here we extend this to a fully fledged minimization algorithm and tool by integrating two new aspects: (1) the computation of the transition structure on the minimized state set, and (2) the computation of the reachable part of the given system. In our generic coalgebraic setting these two aspects turn out to be surprisingly non-trivial requiring us to extend the previous theory. In particular, we identify a sufficient condition on encodings of coalgebras, and we show how to augment the existing interface, which encapsulates computations that are specific for the coalgebraic type functor, to make the above extensions possible. Both extensions have linear run time.

cs.DS↗

arXiv2022

Supported Sets -- A New Foundation For Nominal Sets And Automata

The present work proposes and discusses the category of supported sets which provides a uniform foundation for nominal sets of various kinds, such as those for equality symmetry, for the order symmetry, and renaming sets. We show that all these differently flavoured categories of nominal sets are monadic over supported sets. Thus, supported sets provide a canonical finite way to represent nominal sets and the automata therein, e.g. register automata. Name binding in supported sets is modelled by a functor following the idea of de Bruijn indices. This functor lifts to the well-known abstraction functor in nominal sets. Together with the monadicity result, this gives rise to a transformation process that takes the finite representation of a register automaton in supported sets and transforms it into its configuration automaton in nominal sets.

cs.FL↗

arXiv2022

Minimality Notions via Factorization Systems and Examples

For the minimization of state-based systems (i.e. the reduction of the number of states while retaining the system's semantics), there are two obvious aspects: removing unnecessary states of the system and merging redundant states in the system. In the present article, we relate the two minimization aspects on coalgebras by defining an abstract notion of minimality. The abstract notions minimality and minimization live in a general category with a factorization system. We will find criteria on the category that ensure uniqueness, existence, and functoriality of the minimization aspects. The proofs of these results instantiate to those for reachability and observability minimization in the standard coalgebra literature. Finally, we will see how the two aspects of minimization interact and under which criteria they can be sequenced in any order, like in automata minimization.

cs.FL↗

arXiv2022

A New Approach for Active Automata Learning Based on Apartness

We present $L^{\#}$, a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the $L^{\ast}$ algorithm and its descendants, $L^{\#}$ takes a different perspective: it tries to establish apartness, a constructive form of inequality. $L^{\#}$ does not require auxiliary notions such as observation tables or discrimination trees, but operates directly on tree-shaped automata. $L^{\#}$ has the same asymptotic query and symbol complexities as the best existing learning algorithms, but we show that adaptive distinguishing sequences can be naturally integrated to boost the performance of $L^{\#}$ in practice. Experiments with a prototype implementation, written in Rust, suggest that $L^{\#}$ is competitive with existing algorithms.

cs.FL↗

arXiv2021

Minimality Notions via Factorization Systems

For the minimization of state-based systems (i.e. the reduction of the number of states while retaining the system's semantics), there are two obvious aspects: removing unnecessary states of the system and merging redundant states in the system. In the present article, we relate the two aspects on coalgebras by defining an abstract notion of minimality. The abstract notion minimality and minimization live in a general category with a factorization system. We will find criteria on the category that ensure uniqueness, existence, and functoriality of the minimization aspects. The proofs of these results instantiate to those for reachability and observability minimization in the standard coalgebra literature. Finally, we will see how the two aspects of minimization interact and under which criteria they can be sequenced in any order, like in automata minimization.

cs.FL↗

arXiv2021

Explaining Behavioural Inequivalence Generically in Quasilinear Time

We provide a generic algorithm for constructing formulae that distinguish behaviourally inequivalent states in systems of various transition types such as nondeterministic, probabilistic or weighted; genericity over the transition type is achieved by working with coalgebras for a set functor in the paradigm of universal coalgebra. For every behavioural equivalence class in a given system, we construct a formula which holds precisely at the states in that class. The algorithm instantiates to deterministic finite automata, transition systems, labelled Markov chains, and systems of many other types. The ambient logic is a modal logic featuring modalities that are generically extracted from the functor; these modalities can be systematically translated into custom sets of modalities in a postprocessing step. The new algorithm builds on an existing coalgebraic partition refinement algorithm. It runs in time $\mathcal{O}((m+n) \log n)$ on systems with $n$ states and $m$ transitions, and the same asymptotic bound applies to the dag size of the formulae it constructs. This improves the bounds on run time and formula size compared to previous algorithms even for previously known specific instances, viz. transition systems and Markov chains; in particular, the best previous bound for transition systems was $\mathcal{O}(m n)$.

cs.LO↗

arXiv2021

Nominal Automata with Name Binding

Automata models for data languages (i.e. languages over infinite alphabets) often feature either global or local freshness operators. We show that Bollig et al.'s session automata, which focus on global freshness, are equivalent to regular nondeterministic nominal automata (RNNA), a natural nominal automaton model with explicit name binding that has appeared implicitly in the semantics of nominal Kleene algebra (NKA), an extension of Kleene algebra with name binding. The expected Kleene theorem for NKA is known to fail in one direction, i.e. there are nominal languages that can be accepted by an RNNA but are not definable in NKA; via session automata, we obtain a full Kleene theorem for RNNAs for an expression language that extends NKA with unscoped name binding. Based on the equivalence with RNNAs, we then slightly rephrase the known equivalence checking algorithm for session automata. Reinterpreting the data language semantics of name binding by unrestricted instead of clean alpha-equivalence, we obtain a local freshness semantics as a quotient of the global freshness semantics. Under local freshness semantics, RNNAs turn out to be equivalent to a natural subclass of Bojanczyk et al.'s nondeterministic orbit-finite automata. We establish decidability of inclusion under local freshness by modifying the RNNA-based algorithm; in summary, we obtain a formalism for local freshness in data languages that is reasonably expressive and has a decidable inclusion problem.

cs.FL↗