Constructing solutions to recursive domain equations is a well-known, important problem in the study of programs and programming languages. Mathematically speaking, the problem is finding a fixed point (up to isomorphism) of a suitable functor over a suitable category. A particularly useful instance, inspired by the step-indexing technique, is where the functor is over (a subcategory of) the category of presheaves over the ordinal ω and the functors are locally-contractive, also known as guarded functors. This corresponds to step-indexing over natural numbers. However, for certain problems, e.g., when dealing with infinite non-determinism, one needs to employ trans-finite step-indexing, i.e., consider presheaf categories over higher ordinals. Prior work on trans-finite step-indexing either only considers a very narrow class of functors over a particularly restricted subcategory of presheaves over higher ordinals, or treats the problem very generally working with sheaves over an arbitrary complete Heyting algebras with a well-founded basis.
In this talk we present a solution to the guarded domain equations problem over all guarded functors over the category of presheaves over ordinal numbers, as well as its mechanization in the Rocq proof assistant. As the categories of sheaves and presheaves over ordinals are equivalent, our main contribution is simplifying prior work from the setting of the category of sheaves to the setting of the category of presheaves and mechanizing it — presheaves are more amenable to mechanization in a proof assistant.

Abstract: 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. The proofs are constructive and fully formalized in Agda: https://git8.cs.fau.de/software/initial-algebras-unchained

In this talk, we motivate and define operads. We discuss the relationship of these objects to monads. We turn to the dual problem of constructing cofree coalgebras over operads. We explain how an additional assumption of counitality greatly simplifies the construction. Time permitting, we shall also discuss a simple method of computing the co-Eilenberg-Moore category of comonads arising from certain adjunctions.

The talk is based on the categorical content of some joint work in topology with J. Moreno-Fernández and F. Wierstra, but, barring some examples, no familiarity with homotopy theory will be required.

Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.

(based on joint work with Dan Frumin and Jorge Pérez, presented at CONCUR'24)

We show in this talk that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level ω^ω of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We will see that this problem is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).

Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. It is completely agnostic with respect to the meaning of primitives (keep equivalence decidable) and excludes non-local control flow such as goto, break and return. This limits its application to real-world programs. We introduce control flow GKAT (CF-GKAT), a system that allows control-flow equivalence checking of programs that include non-local control flow as well as hardcoded values.

CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT's abilities, we validated the output of several highly non-trivial program transformations, such as Böhm-Jacopini conversion, and Erosa and Hendren's goto-elimination procedure.

We provide a finite equational presentation of graphs of treewidth at most three, solving an instance of an open problem by Courcelle and Engelfriet.
We use a syntax generalising series-parallel expressions, denoting graphs with a small interface. We introduce appropriate notions of connectivity for such graphs (components, cutvertices, separation pairs). We use those concepts to analyse the structure of graphs of treewidth at most three, showing how they can be decomposed recursively, first canonically into connected parallel components, and then non-deterministically. The main difficulty consists in showing that all non-deterministic choices can be related using only finitely many equational axioms.

We are motivated by explaining the behavioural inequivalence of two states in a finite transition system. Since good explanations are usually concise, our goal is to compute minimal distinguishing behaviour. We use the Hennessy-Milner logic (HML) to express behavioural properties. An HML formula that is satisfied in exactly one of the states is called a distinguishing formula, since it contains behaviour exhibited by one state but not the other. Our goal is to compute a minimal distinguishing formula.
In this talk we show by a reduction to CNF-SAT that computing a minimal distinguishing formula is NP-complete. We relate this result to the earlier algorithms that compute distinguishing formulas that are somewhat minimal. We conclude by showing that we can improve upon the known methods. By using the older inductive notion of bisimilarity we obtain minimal observation-depth, and negation-depth formulas in polynomial time. An implementation shows that the generated formulas are useful as witness even for larger transition systems.

[1] J.J.M. Martens and J.F. Groote. Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. CONCUR 2023, LIPIcs vol. 279.

Among the most celebrated results in category theory is the Lawvere-Linton correspondence theorem relating equational theories in the sense of universal algebra, the algebraic theories of Lawvere, and finitary monads on the category of sets. In this talk, we discuss an extension of the monad-theory part of this correspondence to the setting of graded monads, a generalization of monads given by a stratification of the monad structure in a monoidal category. In detail, we will describe a notion of graded equational theory along with a graded variant of Birkhoff's equational logic. This will allow the formulation of a syntactic characterization of finitary graded monads on sets. Time permitting, I will indicate some details on how graded equational theories can be adapted to the setting of locally presentable categories (e.g. posets, metric spaces, nominal sets, etc.).

Session types are a type discipline to specify and verify communications through protocol descriptions. It has been already 30 years since the first paper on session types, by Kohei Honda at CONCUR 1993. This talk first gives an origin of session types, and then shows the expressiveness results based on the development of a Curry-Howard correspondence with linear logic developed by Perez, Caires, Pfenning and others. It concludes with a different kind of expressiveness, related to choice behaviours of session types.

In this talk, I will discuss the topic of explainability in systems, with a specific emphasis on the intertwined concepts of causality and harm. Causal inference, as formulated by Halpern and Pearl, involves using structural equation models to understand causal relationships between the variables defining a system. This approach employs mathematical representations to capture the causal mechanisms underlying observed behaviours, allowing one to infer cause-and-effect relationships and make predictions about the consequences of interventions or changes to variables in a system. While causal inference and related concepts have emerged as a cornerstone in AI disciplines, I will showcase their expanded role in formal verification contexts. Beyond their applications in AI, I will examine how causal models have been embraced and integrated into Formal Methods (FM), for enhancing system transparency and reliability. Furthermore, I will provide some pointers to the reciprocal relationship between AI and FM, with an emphasis on how FM can contribute to AI's quest for trustworthiness.

To enable compositional reasoning for processes with shared memory, one has to understand how the properties of the behaviour of single processes can be composed into properties of the system that result from letting the processes interact via the shared memory. One option for handling this composition is so-called separation logic, which allows reasoning about memory regions and, thereby, about local views of single processes. This talk investigates compositional reasoning for interacting processes with shared memory. It proposes leveraging sheaves to amalgamate local views of processes into a cohesive specification of the global process, offering a more abstract approach to reasoning. Through a category-theoretic framework, it provides semantics for process interaction via shared memory and establishes connections between sheaves and the semantics of the standard pointer model of separation logic. The talk concludes with an outline of my ongoing research, aiming to refine local reasoning about programs within this framework and extend its applicability to extensions of separation logic.

We study lower bounds for the number of output and equivalence queries required for active learning of finite state machines, focusing on L#. We improve the lower bound of Balcazar et al. (1997) on the combined number of output and equivalence queries required by any learning algorithm, and give a simpler proof. We prove that in the worst case, L# needs n − 1 equivalence queries to learn an FSM with n states, and establish lower bounds on the number of output queries needed by L# in the worst case. In practical applications, the maximum length of the shortest separating sequence for all pairs of inequivalent states (MS3) is often just 1 or 2. We present L#_h , a version of L# with bounded lookahead h, which learns FSMs with an MS3 of at most h without requiring any equivalence queries, and give lower and upper bounds on its complexity.

In the first part of this talk, we characterize the class of nondeterministic ω-automata that can be used for the analysis of finite Markov decision processes (MDPs), such as model checking or reinforcement learning (RL). We call these automata `good-for-MDPs' (GFM). We show that GFM automata are closed under certain simulation relations. We then use simulation to reduce the state space and consider a class of automata particularly suited for RL.

In the second part, we consider using deterministic Streett automata as specifications for MDPs. These occur naturally in many applications, such as the translation of GR(1) properties or the dual of Rabin properties. Unfortunately, Streett automata cannot be used directly for RL. Also, a translation to GFM automata comes at an exponential cost. Surprisingly, we can avoid the exponential cost if we expand the GFM property to alternating automata: The alternating GFM automata we produce from deterministic Streett automata are are of linear size.

Higher-dimensional automata (HDA) are a formalism to model the behaviour of concurrent systems. They are similar to ordinary automata but allow transitions in higher dimensions, effectively enabling multiple actions to happen simultaneously. For ordinary automata, there is a correspondence between regular languages and finite automata. However, regular languages are inherently sequential and one may ask how such a correspondence carries over to HDA, in which several actions can happen at the same time. It has been shown by Fahrenberg et al. that finite HDA correspond with interfaced interval pomset languages generated by sequential and parallel composition and non-empty iteration. In this paper, we seek to extend the correspondence to process replication, also known as parallel Kleene closure. This correspondence cannot be with finite HDA and we instead focus here on locally compact and finitely branching HDA. In the course of this, we extend the notion of interval ipomset languages to arbitrary HDA, show that the category of HDA is locally finitely presentable with compact objects being finite HDA, and we prove language preservation results of colimits. We then define parallel composition as a tensor product of HDA and show that the repeated parallel composition can be expressed as locally compact and as finitely branching HDA, but also that the latter requires infinitely many initial states.

Ω-automata are a type of automata for ω-regular languages. Instead of infinite words, they read pairs of finite words, called lassos, that represent ultimately periodic words. Due to the fact that ω-regular languages are determined by their ultimately periodic fragments, Ω-automata can be associated with ω-regular languages. In terms of structure, they resemble pairs of DFAs, and as a result they can be modelled as coalgebras. We study the categorical relationship between Ω-automata and Wilke algebras, which recognise ω-regular languages. We present a chain of adjunctions starting from the category of Ω-automata and ending in the dual of the category of quotients of the free Wilke algebra. As key ingredients, we determine how the Ω-automata properties circularity and coherence change under transition reversal and propose novel transformations between Ω-automata and Wilke algebras.
This is joint work with Helle Hvid Hansen (University of Groningen) and Clemens Kupke (University of Strathclyde).

Quasitoposes encompass a wide range of structures, including various categories of graphs. They have proven to be a natural setting for reasoning about the metatheory of algebraic graph rewriting. A big challenge is to determine which categories are quasitoposes. In this talk I will explain how endowing presheaves with fuzzy structures form quasitoposes and why that matter, and also how topologies on toposes gives interesting new quasitoposes.

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.
This is joint work with Thorsten Wißmann (FAU Erlangen-Nürnberg).

Communication protocols are a salient approach to the verification of communicating software. In particular, such protocols are typically used for type checking the specification of software. In practice, such specifications are often incomplete, inaccurate, or even inaccessible. In such scenarios, type checking is impossible and other means of verification are necessary. In this talk, I present a framework for the runtime verification of distributed implementations of multiparty communication protocols (global types from multiparty session types). To be precise, we study networks of so-called blackboxes whose behavior we can observe but with unknown specifications. In this framework, each blackbox is coupled with a monitor that is synthesized from a global type. A precise definition allows for the dynamic verification of individual monitored blackboxes, ensuring that the monitored blackbox correctly satisfies the protocol. Our main results are (i) that networks of verified monitored blackboxes sound (they conform to the protocol) and (ii) that monitors are transparent (they interfere minimally with blackbox behavior).
This is joint work with Jorge A. Pérez (Groningen).

This talk is about the Weisfeiler-Leman algorithm. This is an efficient algorithm to colour the vertices (and edges) of a graph in a certain way. It is used as an efficient heuristic to decide graph isomorphism and it was even long thought that it might provide a polynomial algorithm for graph isomorphism (it does not). It was recently observed that this algorithm fits the abstract theory of coalgebraic minimisation. I will explain this connection to coalgebra in detail. However, the real “power” of the WL-algorithm lies in the k-dimensional generalisation and this is harder to relate to coalgebra. We want to understand this from a coalgebraic perspective too, with the hope of bringing results from graph theory to the theory of coalgebra.
The research is work in progress. It is joint work with Tobias Kappé and Thorsten Wißmann.

A communication protocol is realisable if it can be faithfully implemented in a distributed fashion by communicating agents. Pomsets offer a way to compactly represent concurrency in communication protocols and have been recently used for the purpose of realisability analysis. In this paper we focus on the recently introduced branching pomsets, which also compactly represent choices. We define well-formedness conditions on branching pomsets, inspired by multiparty session types, and we prove that the well-formedness of a branching pomset is a sufficient condition for the realisability of the represented communication protocol.

Gentzen's famous cut-elimination algorithm eliminates cuts from a sequent calculus proof to obtain a cut-free proof with the subformula property. This fundamental result is the proof-theoretic starting point for logical investigations. Unfortunately, most substructural and modal logics lack a sequent calculus with cut-elimination. The overwhelming response since the 1960s was to generalise the sequent calculus in a bid to regain cut-elimination but these generalised formalisms are more complicated to reason about and implement.
In this talk I discuss a very different approach called {cut-restriction}: remain in the sequent calculus but restrict the shape/size of those cut-formulas that are ineliminable. I will present an algorithm that subsumes Gentzen's cut-elimination and transforms arbitrary cuts to analytic cuts in many sequent calculi. I will also invite discussion on topics of particular relevance to the NetTCS community: what might be the analogous partial normalisation for natural deduction? What might be its computational interpretation?
This is joint work with Agata Ciabattoni (TU Wien) and Timo Lang (UCL).

We present a compositional model checking algorithm for Markov decision processes, where they are composed in the categorical graphical language of string diagrams. The algorithm computes optimal expected rewards. Our theoretical development of the algorithm is supported by category theory, while what we call decomposition equalities for expected rewards act as a key enabler. Experimental evaluation demonstrates its performance advantages. This talk is based on our joint work with Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo, and will be presented at CAV23.

In programming models with a reversible semantics, computational steps can be undone. In this talk, I discuss the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types.
In prior work, we introduced a monitors-as-memories approach to seamlessly integrate reversible semantics into a process model in which concurrency is governed by session types (a class of behavioral types), covering binary (two-party) protocols with synchronous communication. The applicability and expressiveness of the binary setting, however, is limited. Here we extend our approach, and use it to define reversible semantics for an expressive process model that accounts for multiparty (n-party) protocols, asynchronous communication, decoupled rollbacks, and abstraction passing.
As main result, we prove that our reversible semantics for multiparty protocols is causally-consistent. A key technical ingredient in our developments is an alternative reversible semantics with atomic rollbacks, which is conceptually simple and is shown to characterize decoupled rollbacks.

On streams, a function is said to be causal if the present value of its output is not affected by the future values of its input. A subclass of these causal functions are linear systems over streams, which are closed under sequential and parallel composition and under recursive feedback loops.
In this talk I will introduce three different definitions of causality on cartesian closed categories: as certain morphisms on final coalgebras, as morphisms on final chains (diagrams) and as metric maps.
I will also introduce a traced symmetric monoidal category having diagrams as objects, where streams are special case and linear maps embed into the general framework, while preserving the traced monoidal structure.

Given a labelled transition system, we can talk about its states in terms of logic (which states satisfy which formulas?) and in terms of bisimulation (which states are bisimilar?).
Hennessy and Milner showed that these two views are related: two states satisfy the same formulas precisely when they are bisimilar. In this talk, we look at a directed version of this result: if we assume that every formula true in p is also true in q, what kind of relation does that give between p and q?
This construction is straightforward for Hennessy-Milner logic and strong bisimulation, but is more interesting in the case of Hennessy-Milner Logic with Until and branching bisimulation, where it reveals another, equally expressive, logic that we think corresponds more closely to branching bisimulation.

In the theory of coalgebras, distributive laws give a general perspective on determinisation and other automata constructions. This perspective has recently been extended to include so-called weak distributive laws, covering several constructions on state-based systems that are not captured by regular distributive laws, such as the construction of a belief-state transformer from a probabilistic automaton, and ultrafilter extensions of Kripke frames.
In this talk, we start by recalling the above constructions and their relation to weak distributive laws. We will then discuss how this gives rise to the more general notion of what we call an invertible step: a pair of natural transformations that allows us to move coalgebras along an adjunction. Our main result is then that part of the construction induced by an invertible step preserves and reflects bisimilarity; covering results previously shown by hand for the instances of ultrafilter extensions and belief-state transformers.

The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency.
Central to this approach is the resource consumption paradigm heralded by Linear Logic.
In this talk, we examine this correpsondence and look at a new point in the design space of session type systems based on the Curry-Howard correspondence.
Specifically, we see how the Logic of Bunched Implications (BI) provides a fruitful basis for an interpretation of the logic as a concurrent programming language.
We introduce a new π-calculus with session types based on BI, which leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic.
We will see how fundemental principles of the calculus, like type preservation and deadlock-freedom, are linked to the structural principles of the underlying logic.

Guarded recursion has proved a very robust tool for extending domain theory to many areas, without having to solve the difficult problem of finding classes of CPOs that match a particular problem. The original categorical view on guarded recursion is the so-called topos of trees, which is the category of diagrams in the category of sets reverse-indexed by the ordinal ω. In this talk, I will present some categorical generalisations of guarded recursion: the indexing can be an arbitrary well-founded set (this had been considered in previous work) and we can take diagrams in any category and even in fibrations. This allows us to for example, combine general first- and higher-order logics with guarded recursion. We will also see how to combine computational effects in the form of monads with guarded recursion.