arXiv subjects

Clemens Kupke

Publications and source records attributed to Clemens Kupke.

At least 19 recordsLinked to original sources

arXiv2026

Tree Automata Acceptance up to Measurable Defect

Automata acceptance can, in several situations of interest, be captured game-theoretically via acceptance games. The existence of a winning strategy for Verifier then captures the existence of a winning run-tree of a given automaton over a model. However, such acceptance is rigid, in that it does not allow a measurable defect budget, which can be a challenge in software verification. In this paper, we draw inspiration from how bisimulation distance can be defined as an extension of bisimilarity to define epsilon-acceptance games. Our main theorem shows that a tree T is epsilon-accepted iff there is a tree T' that is accepted in the traditional (rigid) sense and the bisimulation distance of T' and T is at most epsilon. Our work also suggests a strong connection with measure theory, of which we give a preliminary exploration via appropriate examples. Our framework is defined over binary trees with leaves and infinite branches, and strictly contains the case in which binary nodes are seen as probabilistic choice and the defect measures the probability of the set of rejected branches.

cs.LO↗

arXiv2026

Unambiguous Acceptance of Thin Coalgebras

Automata admitting at most one accepting run per structure, known as unambiguous automata, find applications in verification of reactive systems as they extend the class of deterministic automata whilst maintaining some of their desirable properties. In this paper, we generalise a classical construction of unambiguous automata from thin trees to thin coalgebras for analytic functors. This achieves two goals: extending the existing construction to a larger class of structures, and providing conceptual clarity and parametricity to the construction by formalising it in the coalgebraic framework. As part of the construction, we link automaton acceptance of languages of thin coalgebras to language recognition via so-called coherent algebras, which were previously introduced for studying thin coalgebras. This link also allows us to establish an automata-theoretic characterisation of languages recognised by finite coherent algebras.

cs.FL↗

arXiv2025

Constructing Witnesses for Lower Bounds on Behavioural Distances

Behavioural distances provide a robust alternative to notions of equivalence such as bisimilarity in the context of probabilistic transition systems. They can be defined as least fixed points, whose universal property allows us to exhibit upper bounds on the distance between states, showing them to be at most some distance apart. In this paper, we instead consider the problem of bounding distances from below, showing states to be at least some distance apart. Contrary to upper bounds, it is possible to reason about lower bounds inductively. We exploit this by giving an inductive derivation system for lower bounds on an existing definition of behavioural distance for labelled Markov chains. This is inspired by recent work on apartness as an inductive counterpart to bisimilarity. Proofs in our system will be shown to closely match the behavioural distance by soundness and (approximate) completeness results. We further provide a constructive correspondence between our derivation system and formulas in a modal logic with quantitative semantics. This logic was used in recent work of Rady and van Breugel to construct evidence for lower bounds on behavioural distances. Our constructions provide smaller witnessing formulas in many examples.

cs.LO↗

arXiv2025

Relative fixed points of functors

We show how the relatively initial or relatively terminal fixed points for a well-behaved functor $F$ form a pair of adjoint functors between $F$-coalgebras and $F$-algebras. We use the language of locally presentable categories to find sufficient conditions for existence of this adjunction. We show that relative fixed points may be characterized as (co)equalizers of the free (co)monad on $F$. In particular, when $F$ is a polynomial functor on $\mathsf{Set}$ the relative fixed points are a quotient or subset of the free term algebra or the cofree term coalgebra. We give examples of the relative fixed points for polynomial functors and an example which is the Sierpinski carpet. Lastly, we prove a general preservation result for relative fixed points.

math.CT↗

arXiv2025

Thin Coalgebraic Behaviours Are Inductive

Coalgebras for analytic functors uniformly model graph-like systems where the successors of a state may admit certain symmetries. Examples of successor structure include ordered tuples, cyclic lists and multisets. Motivated by goals in automata-based verification and results on thin trees, we introduce thin 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 capture with a single equation when two terms represent the same thin behaviour. Finally, for the special case of polynomial functors, we retrieve from our syntax the notion of Cantor-Bendixson rank of a thin tree.

cs.FL↗

arXiv2025

Expressivity of bisimulation pseudometrics over analytic state spaces

A Markov decision process (MDP) is a state-based dynamical system capable of describing probabilistic behaviour with rewards. In this paper, we view MDPs as coalgebras living in the category of analytic spaces, a very general class of measurable spaces. Note that analytic spaces were already studied in the literature on labelled Markov processes and bisimulation relations. Our results are twofold. First, we define bisimulation pseudometrics over such coalgebras using the framework of fibrations. Second, we develop a quantitative modal logic for such coalgebras and prove a quantitative form of Hennessy-Milner theorem in this new setting stating that the bisimulation pseudometric corresponds to the logical distance induced by modal formulae.

cs.LO↗

arXiv2024

Dual Adjunction Between $Ω$-Automata and Wilke Algebra Quotients

$Ω$-automata and Wilke algebras are formalisms for characterising $ω$-regular languages via their ultimately periodic words. $Ω$-automata read finite representations of ultimately periodic words, called lassos, and they are a subclass of lasso automata. We introduce lasso semigroups as a generalisation of Wilke algebras that mirrors how lasso automata generalise $Ω$-automata, and we show that finite lasso semigroups characterise regular lasso languages. We then show a dual adjunction between lasso automata and quotients of the free lasso semigroup with a recognising set, and as our main result we show that this dual adjunction restricts to one between $Ω$-automata and quotients of the free Wilke algebra with a recognising set.

cs.FL↗

arXiv2024

A Categorical Approach to Coalgebraic Fixpoint Logic

We define a framework for incorporating alternation-free fixpoint logics into the dual-adjunction setup for coalgebraic modal logics. We achieve this by using order-enriched categories. We give a least-solution semantics as well as an initial algebra semantics, and prove they are equivalent. We also show how to place the alternation-free coalgebraic $μ$-calculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality.

cs.LO↗

arXiv2024

Proving Behavioural Apartness

Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems. We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples.

cs.LO↗

arXiv2023

Beyond Initial Algebras and Final Coalgebras

We provide a construction of the fixed points of functors which may not be inital algebras or final coalgebras. For an endofunctor F, this fixed point construction may be expressed as a pair of adjoint functors between F-coalgebras and F-algebras. We prove a version of the limit colimit coincidence theorem for these generalized fixed points.

math.CT↗

arXiv2021

Expressive Logics for Coinductive Predicates

The classical Hennessy-Milner theorem says that two states of an image-finite transition system are bisimilar if and only if they satisfy the same formulas in a certain modal logic. In this paper we study this type of result in a general context, moving from transition systems to coalgebras and from bisimilarity to coinductive predicates. We formulate when a logic fully characterises a coinductive predicate on coalgebras, by providing suitable notions of adequacy and expressivity, and give sufficient conditions on the semantics. The approach is illustrated with logics characterising similarity, divergence and a behavioural metric on automata.

cs.LO↗

arXiv2021

Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics

We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka's linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e. in coalgebraic hybrid logic.

cs.LO↗

arXiv2021

Learning Weighted Automata over Principal Ideal Domains

In this paper, we study active learning algorithms for weighted automata over a semiring. We show that a variant of Angluin's seminal \LStar\ algorithm works when the semiring is a principal ideal domain, but not for general semirings such as the natural numbers.

cs.FL↗

arXiv2021

On the size of disjunctive formulas in the $μ$-calculus

A key result in the theory of the modal mu-calculus is the disjunctive normal form theorem by Janin & Walukiewicz, stating that every mu-calculus formula is semantically equivalent to a so-called disjunctive formula. These disjunctive formulas have good computational properties and play a pivotal role in the theory of the modal mu-calculus. It is therefore an interesting question what the best normalisation procedure is for rewriting a formula into an equivalent disjunctive formula of minimal size. The best constructions that are known from the literature are automata-theoretic in nature and consist of a guarded transformation, i.e., the constructing of an equivalent guarded alternating automaton from a mu-calculus formula, followed by a Simulation Theorem stating that any such alternating automaton can be transformed into an equivalent non-deterministic one. Both of these transformations are exponential constructions, making the best normalisation procedure doubly exponential. Our key contribution presented here shows that the two parts of the normalisation procedure can be integrated, leading to a procedure that is single-exponential in the closure size of the formula.

cs.LO↗

arXiv2021

Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation

A modal logic that is strong enough to fully characterize the behavior of a system is called expressive. Recently, with the growing diversity of systems to be reasoned about (probabilistic, cyber-physical, etc.), the focus shifted to quantitative settings which resulted in a number of expressivity results for quantitative logics and behavioral metrics. Each of these quantitative expressivity results uses a tailor-made argument; distilling the essence of these arguments is non-trivial, yet important to support the design of expressive modal logics for new quantitative settings. In this paper, we present the first categorical framework for deriving quantitative expressivity results, based on the new notion of approximating family. A key ingredient is the codensity lifting -- a uniform observation-centric construction of various bisimilarity-like notions such as bisimulation metrics. We show that several recent quantitative expressivity results (e.g. by König et al. and by Fijalkow et al.) are accommodated in our framework; a new expressivity result is derived, too, for what we call bisimulation uniformity.

cs.LO↗

arXiv2021

Compositional Game Theory, Compositionally

We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to build new Arrows from old. We model equilibria as a bimodule over an Arrow and define an operator to build a new Arrow from such a bimodule over an existing Arrow. We also model strategies as graded Arrows and define an operator which builds a new Arrow by taking the colimit of a graded Arrow. A final operator builds a graded Arrow from a graded bimodule. We use this compositional approach to CGT to show how known and previously unknown variants of open games can be proven to form symmetric monoidal categories.

cs.LO↗

arXiv2020

Size matters in the modal $μ$-calculus

We discuss and compare complexity measures for the modal $μ$-calculus, focusing on size and alternation depth. As a yardstick we take Wilke's alternating tree automata, which we shall call parity formulas in the text. Building on work by Bruse, Friedmann & Lange, we compare two size measures for $μ$-calculus formulas: subformula-size,i.e. , the number of subformulas of the given formula, and closure-size. These notions correspond to the representation of a formula as a parity formula based on, respectively, its subformula dag, and its closure graph. What distinguishes our approach is that we are explicit about the role of alpha-equivalence, as naively renaming bound variables can lead to an exponential blow-up. In addition, we match the formula's alternation depth with the index of the parity formula. We start in a setting without alpha-equivalence. We define subformula-size and closure-size and recall that a $μ$-calculus formula can be transformed into a parity formula of size linear wrt subformula size, and give a construction that transforms a $μ$-calculus formula into an equivalent parity formula linear wrt closure-size. Conversely, there is a standard transformation producing a $μ$-calculus formula of exponential subformula -- but linear closure-size in terms of the size of the original parity formula. We identify so-called untwisted parity formulas for which a transformation linear in subformula-size exists. We then introduce size notions that are completely invariant under alpha equivalence. We transfer the result of Bruse et alii, showing that also in our setting closure-size can be exponentially smaller than subformula-size. We also show how to rename bound variables so that alpha-equivalence becomes syntactic identity on the closure set. Finally, we review the complexity of guarded transformations.

cs.LO↗

arXiv2020

Compositional Game Theory with Mixed Strategies: Probabilistic Open Games Using a Distributive Law

We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show that the resulting games form a symmetric monoidal category, which can be used to compose probabilistic games in parallel and sequentially. We also consider morphisms between games, and show that intuitive constructions give rise to functors and adjunctions between pure and probabilistic open games.

cs.LO↗