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.