# A categorical and logical framework for iterated protocols

Eric Goubault, Roman Kniazev, Bernardo Hummes, Jérémy Ledent, Sergio Rajsbaum

## ► To cite this version:

Eric Goubault, Roman Kniazev, Bernardo Hummes, Jérémy Ledent, Sergio Rajsbaum. A categorical and logical framework for iterated protocols. 2025. hal-05068745

HAL Id: hal-05068745

https://polytechnique.hal.science/hal-05068745v1

Preprint submitted on 15 May 2025

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published or not. The documents may come from teaching and research institutions in France or abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est destinée au dépôt et à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A categorical and logical framework for iterated protocols

**Eric Goubault**

LIX
CNRS, École polytechnique, IP Paris
91120 Palaiseau, France

**Roman Kniazev**

LaBRI
CNRS, Université de Bordeaux
33405 Talence, France

**Sergio Rajsbaum**

Instituto de Matemáticas
Universidad Nacional Autónoma de México
04510 Mexico City, Mexico

**Bernardo Hummes Flores**

LIX
CNRS, École polytechnique, IP Paris
91120 Palaiseau, France

**Jérémy Ledent**

IRIF
CNRS, Université Paris Cité
75013 Paris, France

**Abstract.** In this article, we show that the now classical protocol complex approach to distributed task solvability of Herlihy et al. [1] can be understood in standard categorical terms. First, protocol complexes are functors, from chromatic (semi-) simplicial sets to chromatic simplicial sets, that naturally give rise to algebras. These algebras describe the next state operator for the corresponding distributed systems. This is constructed for semi-synchronous distributed systems with general patterns of communication for which we show that these functors are always Yoneda extensions of simpler functors, implying a number of interesting properties. Furthermore, for these protocol complex functors, we prove the existence of a free algebra on any initial chromatic simplicial complex, modeling iterated protocol complexes. Under this categorical formalization, protocol complexes are seen as transition systems, where states are structured as chromatic simplicial sets. We exploit the epistemic interpretation of chromatic simplicial sets [2] and the underlying transition system (or algebra) structure to introduce a temporal-epistemic logic and its semantics on all free algebras on chromatic simplicial sets. We end up by giving hints on how to extend this framework to more general dynamic network graphs and state-dependent protocols, and give example in fault-tolerant distributed systems and mobile robotics.
**Keywords:** Distributed systems, protocol complex, algebras and co-algebras, free algebras, temporal logics, epistemic logics.

**ACM subject classification:** CCS→Theory of computation→Models of computation→Concurrence→Distributed computing models; CCS→Theory of computation→Logic→Modal and temporal logics; CCS→Theory of computation→Logic→Logic and verification

# 1. Introduction

One of the great successes in formal methods for programming languages is the use of temporal logics [3] for specifying and verifying sequential systems. This has been originally based on linear-time temporal logics (LTL), in which the progress of execution is identified with a step number, an integral number. The semantics of LTL is easily given in full generality on transition systems (Kripke structures of some particular sort), where next step and until operators are easily interpretable. This makes it possible to relate LTL properties with sequential programs, whose semantics are classically given in terms of transition systems.

In distributed systems, many specification and verification frameworks have been proposed, for different application areas, e.g. linearizability [4] for concurrent data structures, task specifications [5, 6] for fault-tolerant distributed protocols (e.g. consensus), partial unifications such as the ones of [7, 8], etc. but seem to elude the world of logics and model-checking, at the notable exception of [9] using epistemic logics and [10] for concurrent systems.

In this paper, we show how to build on the success of epistemic logics for multiagent systems and of temporal logics for concurrent systems, so as to get a temporal-epistemic logics suited to round-based wait-free distributed systems. The main observation of the paper, that makes this possible, is to see that the protocol complex approach to distributed computability [1] can be naturally recast as particular functors $F$ from chromatic semi-simplicial sets to chromatic simplicial sets. These chromatic semi-simplicial sets represent the set of potential global states of the distributed system at some round of communication, and this “protocol complex functor” $F$ produces from this set of global states, the set of potential next states, still organized within a chromatic semi-simplicial set. Under some mild assumptions, we show that this functor $F$ is naturally a Yoneda extension of a simpler functor, hence exhibits numerous interesting categorical properties. Moreover, we show that this naturally produces a $F$-algebra, and that the interesting categorical properties of $F$ we were mentioning imply that there is always free $F$-algebras. This allows for formalizing nicely iterated protocol complexes, and for deriving the semantics of a temporal-epistemic logics that formalizes the temporal evolution of the knowledge within such round-based distributed systems. This is based on previous work [11, 12, 13] showing that chromatic semi-simplicial sets provide natural semantics to epistemic logics.

**Contents** We begin by giving the necessary background material in Section 2, to set up the scene on (categorical) algebras and co-algebras, and in Section 3, with distributed protocols and the use of simplicial complexes and sets as formalizations of their states.
We then show in Section 4, informally at first, that these protocol complexes naturally give rise to
functors, and even very particular functors in the case of oblivious protocols that are Yoneda extensions
of simple functors defined on sets of participating processes.

The protocol complex functor encodes the set (or simplicial set) of states that are reachable after
one step of communication, from some given set (or, more precisely again, simplicial set) of initial
states. The way the next states are linked to any particular initial state is through a simplicial set
morphism from the protocol complex to the initial complex, meaning that the transition to next states
can be encoded in algebras, similarly to the case of more classical transition systems. This is developed
in Section 5, where we also mention a co-algebraic view, that comes for free due to the fact our protocol
complex functors always admit a right adjoint.

We then prove in Section 6 that our protocol complex functors always admit free algebras, which
allows for naturally formalizing iterated protocols.

We introduce in Section 7 a temporal-epistemic logics which is particularly well suited to an
interpretation in free algebras. It naturally extends DEL as used for particular protocols [14] and give
a few examples of potential applications to distributed systems and mobile robotics.

Finally, in Section 8, we give hints about how to generalize this work to non-oblivious protocols.
This includes, in particular, general dynamic networks [15] and mobile robots.

**2. Algebras (and co-algebras) and sequential systems, a reminder**

Algebras, in the category-theoretic sense [16], appear in a number of situations. For instance, any
deterministic transition system can be seen as an algebra over a certain endofunctor on the category of
sets. Given a set Ac of “actions”, consider the endofunctor F on sets X ↦→ X × Ac. Then a function
A : X × Ac → X gives rise to an automaton: indeed, given a pair (x, a), where x is interpreted as
a state and a as an action, the function A assigns to this pair another state x', the end-point of the
transition. This construction is an instance of an F-algebra that we define below:

**Definition 2.1. (F-algebra)**

Let $F$ be an endofunctor on a category $C$, $F : C \to C$. An $F$-algebra is a pair $(C, a : F(C) \to C)$ where $C \in C$ and $a$ is a morphism in $C$, called the *algebra structure of* $C$.

Let $(C, a)$ and $(C', a')$ be two $F$-algebras. Then $f$ is a morphism of $F$-algebras from $(C, a)$ to $(C', a')$ if and only $f$ is a morphism from $C$ to $C'$ in $C$ and the following diagram commutes:

<figure><img src="image_2.png" /></figure>

The category of $F$-algebras is denoted by $Alg(F)$.
There is a dual notion of a co-algebra, which is an algebra in the opposite category, that is, the direction of the morphisms is reversed. We will touch upon the subject only in Section 5.2, in which we mention the cases where we have the same “object” being both an *F*-algebra and a *G*-co-algebra, for some functor *G* related to *F* (this will be the case for our models of distributed systems).

In their seminal work [17], Adámek and Porst argue that, to model sequential systems via *F*-algebras, it is desirable for the endofunctor *F* to admit free algebras. That is, for every object *I*, there should exist a free *F*-algebra generated by *I*:

**Definition 2.2. (Free F-algebra)**

Given an endofunctor $F : C \to C$ and an object $I$ in $C$, an $F$-algebra $(I^\infty, \phi_I)$ together with a morphism $\eta : I \to I^\infty$ is said to be a free $F$-algebra generated by $I$ if the following condition holds: for each $F$-algebra $(Q, q)$ and each morphism $f : I \to Q$ there is a unique morphism of $F$-algebras $f^* : (I^\infty, \phi_I) \to (Q, q)$ such that $f = f^* \circ \eta$:

<figure><img src="image_3.png" /></figure>

An endofunctor $F : C \to C$ is a *variety* [17] if there is always a free $F$-algebra generated by any $I \in C$.

Said in another manner, first note that for all endofunctors $F : C \to C$, there is a forgetful functor $U : \mathrm{Alg}(F) \to C$, which to every $F$-algebra $(C, a : F(C) \to C)$ associates $C$ in $C$. Then $F$ is a variety if the forgetful functor $U$ has a right adjoint. This right adjoint, when it exists, is the one that associates with each $C \in C$ the free $F$-algebra on $C$.

The algebraic view of deterministic transition systems naturally leads to varieties. Consider again the functor $F$ which to any set $X$ associates $X \times Ac$, and a set $S$. Then the free algebra generated by $S$ exists and is given by formula_1

$$S^{\infty} = S \cup \bigcup_{n>0} S \times A c^{n} \qquad (1)$$

and morphism $\Phi_I : S^\infty \times Ac \to S^\infty$ sends a triple that consists of a state $s$, a sequence of actions $\langle a_1 a_2 \dots a_n \rangle$, and another action $a$ to a pair $(s, \langle a_1 \dots a_n a \rangle)$.

An interesting consequence of Definition 2.2 is that, for a variety $F$, for any $F$-algebra $q : F(I) \to I$, there exists a unique morphism in $C$ such that the following diagram commutes:

<figure><img src="image_4.png" /></figure>

Consider the following maps:

$$g_i = q \circ F(q) \circ \dots \circ F^{i-2}(q) \circ F^{i-1}(q) : F^i(I) \to I$$
In the case of the deterministic transition systems above, it is easy to see that $g_i$ acts as follows:

$$g_i(s, \langle a_1 a_2 \dots a_i \rangle) = q(q(\dots q(s, a_1), a_2), \dots, a_i)$$

This shows the usefulness of the notion of free algebra, which makes it possible to iterate on the transition function (in the case of deterministic transition systems), i.e. to take the “most universal” algebra that “completes” the original set of states with all states that are reachable by taking a finite (but unbounded) number of transitions.

Indeed, this is a construction of a least fixed point, applied to the “one-step” transition function defined by the functor $F$. Classical set-based (or poset-based) semantics use Tarski theorem to prove the existence of such fixed points, and Kleene theorem when applicable, to give explicit formulas for least fixed points, under some mild hypotheses. Indeed, we recognize in Equation (1) a Kleene type of formula.

As we will not use endofunctors on Set, but on more general categories, and in particular simpli- cial complexes (Section 3.1) and simplicial sets (Section 3.3) we need some generalization of these theorems, that we give below (first a Tarski-like one, and then a Kleene-like one).

**Lemma 2.3. (see [18])**

Given a functor $F: C \to C$ that preserves monomorphisms, the following is equivalent for any object $I$ in $C$:

* There exists a free $F$-algebra generated by $I$;

* There exists an object $X$ isomorphic to $I + FX$.

A statement more precise than Lemma 2.3 can be obtained for an endofunctor $F$ that commutes with colimits.

**Theorem 2.4.** Let $F: C \to C$ be a functor that commutes with colimits and that preserves monomor- phisms. Then for any object $I \in C$ there exists a free $F$-algebra generated by $I$, which is given as follows. Let $I^\infty$ be the infinite coproduct:

$$I^\infty = I \coprod F(I) \coprod \dots \coprod F^n(I) \coprod F^{n+1}(I) \dots$$

As $F$ commutes with colimits, $F(I^\infty)$ is isomorphic to $\coprod_{i \ge 1} F^i(I)$ and we denote by $\phi_I$ the map induced by the identities on each $F(F^{n-1}(I)) = F^n(I) \subseteq F(I^\infty)$ to $F^n(I) \subseteq I^\infty$.

**Proof:**

We use the free algebra construction of [18] and Lemma 2.3. □

<figure><img src="image_5.png" /></figure>

We are now going to exploit this generalized semantical framework to recognize a pattern similar to deterministic transition systems in the definition and use of protocol complexes, modeling certain distributed machines, that we are introducing in next section.
3. Background on simplicial complexes for distributed computing and epistemic logic

This section presents background on distributed computing and its relation to combinatorial topology (simplicial complexes and simplicial sets) as well as epistemic logics. It focuses on models where computation can be organized in layers [19], including asynchronous and synchronous models where processes (agents in distributed computing systems) can fail by crashing.

**3.1. Chromatic simplicial complexes and distributed computation**

There is an intimate relationship between distributed computing and (combinatorial) topology, that has been thoroughly studied [1]. The basic idea is to represent the final global states of a protocol as a simplicial complex, notion that we now recap below.

**Simplicial complexes** A simplicial complex $K = (V, S)$ consists of a set $V$, together with a family $S$ of non-empty finite subsets of $V$ such that for all $X \in S$, $Y \subseteq X$ implies $Y \in S$. An element of $V$ is called a *vertex* (plural vertices), and an element of $S$ is a *simplex* (plural simplices). When two simplices $X, Y \in S$ are such that $Y \subseteq X$, we say that $Y$ is a *face* of $X$. Simplices that are maximal w.r.t. inclusion are called *facets*. The *dimension* of a simplex $X \in S$ is $|X| - 1$, and a simplex of dimension $n$ is called an *$n$-simplex*. Simplices of dimension 0, 1 and 2 are also called vertices, edges and triangles, respectively. Thus, we often identify a vertex $v \in V$ with the 0-simplex $\{v\} \in S$.

A simplicial complex $K$ is *pure* if all its facets are of the same dimension, $n$. In this case, we say that $K$ is of dimension $n$. Given a set $A$ of processes (that we will represent as colors), a *chromatic simplicial complex* $K = (V, S, \chi)$ consists of a simplicial complex $(V, S)$ together with a coloring map $\chi: V \to A$, such that for all $X \in S$, all the vertices of $X$ have distinct colors.

Let $K$ and $K'$ be two simplicial complexes. A *simplicial map* (a.k.a. *morphism*) $f: K \to K'$ sends the vertices of $K$ to vertices of $K'$, such that if $X$ is a simplex of $K$, then $f(X)$ is a simplex of $K'$. When $K$ and $K'$ are chromatic, a *chromatic simplicial map* must additionally preserves colors.

**Protocol complexes and task solvability.** In the formalization of distributed systems of e.g. [1], a system comprised of $n$ processes running concurrently is modeled by a pure chromatic simplicial complex of dimension $n$, called the *protocol complex*. Each global state corresponds to a facet, and each vertex of this facet corresponds to the local states of one process. Thus, each vertex is labeled with a process id, which is why this construction gives rise to a chromatic simplicial complex. The remarkable connection with topology comes from the fact that, when processes communicate with each other, and the simplicial complex of global states evolves over time, some topological invariants are preserved. These topological invariants in turn determine the computational power of the system.

The area of fault-tolerant distributed computing is concerned with determining which tasks are
solvable in various computational models. In the topological approach of [1], the following notion of
task solvability is used. A task $\mathcal{T}$ is given by the following data:

• a chromatic simplicial complex of inputs $I$, called the *input complex*;
• a chromatic simplicial complex of outputs O, called the *output complex*;

• a *task specification* *T*, which is a sub-complex of *I* × *O*. This chromatic simplicial complex *T* relates inputs with potential outputs, that any protocol solving the task should choose from. Naturally, *T* comes with a projection morphism π<sub>*T*</sub> : *T* → *I*.

Given a particular architecture of communication, and an input complex *I*, we can produce the *protocol complex* that consists of all global states that are reachable from an input of *I* after one round of communication. When we consider several rounds of communication, this is called the *iterated protocol complex*: the complex of global states at the end of the first round of communication, can be used as the input complex from which the second round of communication is performed.

Given such a (possibly iterated) protocol complex *P*, because of its construction (which is formalized in Section 5) there is always a simplicial map $\pi_P : P \to I$ that relates every global state of *P* (i.e., every simplex) to the inputs of *I* that it was computed from.

We can now define the notion of task solvability. A task $\mathcal{T}$ is solvable using the (possibly iterated) protocol complex $P$ if there exists a chromatic simplicial morphism $\delta : P \to T$ such that $\pi_I \circ \delta = \pi_P$, i.e., the diagram of simplicial complexes below commutes.

<figure><img src="image_6.png" /></figure>

The intuition behind this definition is the following. A facet *X* in *P* corresponds to a global state that is reachable from input $\pi_P(X)$ in *I*. The morphism $\delta$ sends *X* to a facet $\delta(X) = (X_I, X_O)$ of *T*: crucially, every vertex of *X* (that is, every local state of a process) is assigned an output value in $X_O \subseteq O$. The commutativity of the diagram expresses the fact that both *X* and $\delta(X)$ correspond to the same input assignment $X_I = \pi_P(X)$. The fact that $\delta(X) = (X_I, X_O)$ is a simplex of *T* ensures that the chosen set of outputs is compatible with the set of inputs according to the task specification. Finally, the fact that simplicial maps act on vertices means that a process must decide its output value based only on its local state. When one vertex (local state) belongs to two or more simplices (global states), this means that the two global states are *indistinguishable* from the point of view of this process: it must choose the same output value in both situations.

**3.2. Chromatic simplicial complexes as simplicial models for epistemic logics**

The usual S5<sub>n</sub> epistemic logic for a multi-agent system has the following syntax. Let *AP* be a countable set of atomic propositions and *A* a finite set of agents. The language of epistemic logic formulas *L*<sub>*K*</sub>(*A*, *AP*), or just *L*<sub>*K*</sub> if *A* and *AP* are left implicit, is generated by the following BNF grammar:

$$
\varphi ::= p \mid \neg \varphi \mid (\varphi \land \varphi) \mid K_a \varphi \quad p \in AP, a \in A
$$
We are also interested in epistemic logic with *common knowledge* operators. We write $\mathcal{L}_{CK}(A, AP)$ for the language of these formulas, defined by:

$$ \varphi ::= p \mid \neg \varphi \mid (\varphi \wedge \varphi) \mid K_a \varphi \mid C_B \varphi \quad p \in AP, a \in A, B \subseteq A $$

Recall that usually, an $S5_n$ epistemic model is based on a *Kripke frame*, a graph whose nodes are the possible worlds, and whose edges are labeled with agents that cannot distinguish between two worlds. A *Kripke model* is obtained by labeling the nodes of the graph with sets of atomic propositions. Much work exists on using Kripke models to reason about distributed computing [9], we are more interested here instead on using simplicial complex models instead.

An epistemic logic framework to model the topology approach to distributed computing was presented in [11]. To do so, Kripke models are replaced by a dual notion of *simplicial complex models*. In fact, there is an equivalence of categories between Kripke models and simplicial models. Thus, simplicial models retain the properties of Kripke models, such as soundness and completeness w.r.t. to the logic $S5_n$. Furthermore, this simplicial approach to epistemic logic can be extended to *dynamic epistemic logic* (DEL) [20, 21], using a simplicial version of *action models* [22].

### 3.3. Chromatic (augmented semi-)simplicial sets

Unfortunately, chromatic simplicial complexes are rather inconvenient in categorical terms, whereas chromatic (semi-)simplicial sets are both more general and much better behaved. Chromatic semi-simplicial sets, or csets, have already been studied in the context of distributed computing in [13].

Let us start with an intuitive explanation of what is a chromatic semi-simplicial set. Recall that, to define a simplicial complex, one must provide a set $V$ of vertices; and then an $n$-simplex of higher dimension is identified with its set of $n+1$ vertices. In contrast, to define a semi-simplicial set, we directly give the set $S_n$ of $n$-simplices for every $n$. To describe how those basic blocks are “glued together” into a geometric structure, we moreover need to define face maps of the form $\partial_n^i : S_n \to S_{n-1}$, mapping every $n$-simplex to its $(n-1)$-dimensional faces. In fact, we do something a little bit more unusual here: we add colors to the definition. Instead of having a set $S_n$ of $n$-simplices for every dimension $n$, we will have a set $X(U)$ of $U$-colored simplices for every set of colors $U \subseteq A$. This yields the definition of *chromatic semi-simplicial sets*.

We start by giving a slick formal definition of the category of csets as a category of presheaves. We will then unpack the data to give a more concrete definition. As with the site of semi-simplicial sets (see e.g., [23, 24]), the site of chromatic augmented semi-simplicial sets is a posetal category $\Gamma$, which is the category of subsets of $A$ with the inclusion partial order, defined below.

**Definition 3.1. (The category $\Gamma$)**

Given a set $A$ of processes, the category $\Gamma$ is such that:

* Its objects are (possibly empty) subsets of $A$.

* There is a unique morphism $\delta_{U,V} : U \to V$ in $\Gamma$ whenever $U \subseteq V$. Composition $\delta_{V,W} \circ \delta_{U,V} = \delta_{U,W}$ is given by the fact that $U \subseteq V \subseteq W$ implies $U \subseteq W$.
The category of chromatic augmented semi-simplicial sets, or cset for short, is the category $\Gamma^{\text{op}}\text{Set}$ of presheaves on $\Gamma$. Hence a cset is defined as a functor $X : \Gamma^{\text{op}} \to \text{Set}$, and morphisms of csets are natural transformations between such functors.

Given a cset $X \in \Gamma^{\text{op}}\text{Set}$, and a group of processes $U \subseteq A$, the elements of $X(U)$ are called the *U-simplices*. When there is no ambiguity, we write $\partial_{U,V} : X(V) \to X(U)$ for the boundary operator $X(\delta_{U,V})$. For $x \in X(V)$ a V-simplex, $\partial_{U,V}(x)$ is called the *U-face* of $x$. If it is clear which $V$ is considered, we simply write $\partial_U(x)$. The standard U-simplex $\Gamma[U]$, for some set of processes $U \subseteq A$, is defined as the representable presheaf $\Gamma(-, U)$, image of $U$ by the Yoneda embedding $y : \Gamma \to \Gamma^{\text{op}}\text{Set}$.

Let us unpack these definitions. A cset $X$ consists of a family of sets $X(U)$ for every $U \subseteq A$, together with a family of maps $\partial_{U,V} : X(V) \to X(U)$ for every $U \subseteq V \subseteq A$. Intuitively, from any $V$-simplex (i.e., a simplex whose vertices are colored by $V$), we can extract its $U$-face by keeping only the vertices whose color belongs to $U$. These face maps must moreover be compatible, in the sense that if $U \subseteq V \subseteq W$, then $\partial_{U,V} \circ \partial_{V,W} = \partial_{U,W}$. The standard $U$-simplex $\Gamma[U]$ has a unique $T$-simplex for every $T \subseteq U$; and no $T$-simplex for $U \not\subseteq T$. That is, $\Gamma[U](T)$ is a singleton set for each $T \subseteq U$, and is the empty set otherwise. The face maps of $\Gamma[U]$ are trivial since all sets are singletons. Geometrically, $\Gamma[U]$ can be viewed as a single simplex with vertices colored by $U$, and all of its faces.

**Example 3.2.** A cset $X$ is depicted in the figure below. We represent it as a semi-simplicial set together with colors on the vertices. Let us write $A = \{r, g, b\}$ for the set of colors (red, green, blue). The two elements of $X(\{r, g, b\})$ are depicted as triangles, whose vertices colored in red, green and blue. The sets $X(\{r, g\})$ and $X(\{g, b\})$ both contain three elements, depicted as edges (with the corresponding colors on the vertices); while the set $X(\{r, b\})$ only contains two elements (the two parallel red/blue edges). The sets $X(\{r\})$, $X(\{g\})$ and $X(\{b\})$ contain respectively two, three, and two elements; depicted as red, green and blue vertices. Finally, the set $X(\emptyset)$ contains two elements, represented as dashed regions (they can be interpreted as a notion of generalized connected components). The face maps $\partial_U$ for $U \subseteq \{r, g, b\}$ give the equations that permit to glue together all of these simplices, along lower dimensional simplices.

<figure><img src="image_7.png" /></figure>

In [13], csets have been used to model distributed computing protocols. As with simplicial complexes, the vertices represent local states of individual agents (processes) $a \in A$, and its color, representing the name of the process. Maximal simplexes (i.e., facets) correspond to global states of the system. What is new with the semi-simplicial set approach is that we can also explicitly model information in-between the two: $U$-simplexes represent the combined states of a set $U$ of participating processes. This is closely linked to the notion of *distributed knowledge*, where a set of agents is viewed as a single entity that can collectively know some facts about the possible worlds.
4. Protocol complex functors for round-based oblivious distributed sys-
tems

The protocol complex that appears in fault-tolerant distributed computing can be formally defined a particular functorial construction, at least for round-based oblivious systems, as we now describe. The advantage of our functorial definition is that it highlights the modular structure of the protocol complex: one only needs to specify what happens to a single simplex (i.e., global state), for one round of computation. From this, the protocol complex can be derived for any input complex and any number of rounds. This can be constructed, and studied, under the following (informal for now) assumptions. We hint at further generalizations in Section 8.

1. Communication is *round-based*. This means that protocols are structured as a sequence of rounds, where processes communicate with each other, potentially with faults occurring. Note that this does not necessarily imply synchrony: for instance, the immediate snapshot model of Section 4.2 exhibits a round structure, even though it can be implemented in a fully asynchronous way. Indeed, some processes are allowed to start subsequent rounds even though some other processes are still in the previous rounds; and they do so in a fresh memory array to avoid interfering. In such cases, a slow process is indistinguishable from a crashed process.

2. Communication is *oblivious*. We assume that the communication patterns that can occur do not depend on the values of local states of processes. This means that the “set” (actually a simplicial complex or a cset) of states that are reachable from a given global state only depends on the set of participating processes, and not on the actual values held by the processes.

3. Communication is *wait-free*. At any point in time, we always consider the possibility that only a subset of the currently active processes will participate in the next round (either because the other processes are slow, or have crashed). So if a set *A* of processes are active, and *B* ⊆ *A*, performing one round of communication within the set *A* must also include the effect of communication on the smaller set of processes *B*.

With these hypotheses, protocol complexes play the role of automata in our formalization, as shown by the algebraic formulation that we develop now. For distributed computing, we are dealing with algebras over an endofunctor on chromatic simplicial complexes (or chromatic simplicial sets, as explained in Section 3.3). This differs from the usual setting of sequential computation and ordinary automata, which are algebras on sets. In logical and categorical terms, this is similar though, since csets form a topos which are a categorical generalization of sets [25].

**4.1. The protocol complex functor**

Hypotheses 1 and 2 above indicate that we only need to specify the protocol complex for a single initial state and a single round of communication. Thus, all relevant information should lie within a functor $F : \Gamma \to \Gamma^{\text{opSet}}$, where the objects of $\Gamma$ encode the possible sets of participating processes. Hypothesis 3 indicates that this functor $F$ should be monotonic, in the sense that $F$ preserves monomorphisms (both in $\Gamma$ and in $\Gamma^{\text{opSet}}$, monomorphisms are inclusions).
Once such a $F$ is defined, we can extend it in a canonical way to a functor $F_! : \Gamma^{\text{op}}\mathbf{Set} \to \Gamma^{\text{op}}\mathbf{Set}$ that acts on an input complex, consisting of many global states glued together. This extension of the functor $F$ is a classic categorical construction called a Yoneda extension, that we recall below.

**Lemma 4.1. (see [26])**

Let $B$ be a small category, $C$ a category. Every functor $F : B \to C$ defines a functor $F^* : C \to B^{\text{op}}\mathbf{Set}$ defined on the objects $c$ in $C$ by $F^*(c) = \text{Hom}_C(F-, c)$. If $C$ has small direct limits (also called filtered limits in [16]) then $F^*$ has a left adjoint $F_! : B^{\text{op}}\mathbf{Set} \to C$ which is the unique<fnref n="1" /> functor commuting with direct limits such that $F_!(B[b]) = F(b)$ for all $b \in B$ (where, as before, the notation $B[b]$ denotes the representable functor $\text{Hom}_B(-, b)$).

Moreover, there is an equivalence of categories between the category of functors from $B$ to $C$, and the full subcategory of the category of functors from $B^{\text{op}}\mathbf{Set}$ to $C$ consisting of those functors that commute with direct limits.

When particularizing Lemma 4.1 to the context of chromatic augmented simplicial sets and distributed computing, it reads as follows. Consider a functor $F : \Gamma \to \Gamma^{\text{op}}\mathbf{Set}$ specifying the way the one-round protocol complex operator acts on a single global state with a set $U \subseteq A$ of participating processes. Then $F_! : \Gamma^{\text{op}}\mathbf{Set} \to \Gamma^{\text{op}}\mathbf{Set}$ extends $F$ to all chromatic augmented semi-simplicial sets (and not just the standard $U$-simplex $\Gamma[U]$ alone), commutes with colimits, and therefore defines the effect of one-round communication for any set of combined global states. Note that even though we are mainly interested in the functor $F_!$, Lemma 4.1 also gives “for free” a right adjoint to $F_!$, called $F^*$. We will not make use of the functor $F^*$ to study protocol complexes, but it might be worth studying what this functor means in the context of distributed computing.

**4.2. A first example: the asynchronous immediate snapshot model**

Let us consider processes that communicate by reading and writing asynchronously into a shared memory. Let us assume that the set of participating processes is $A = \{a_1, \dots, a_n\}$. Each process $a_i$ holds a private value called its a local state, $v_i$. The shared memory consists of a sequence of shared arrays of size $n$, one for each round. Thus, at round $k$, we use a fresh array $x^k$ consisting of $n$ memory locations $x_1^k, \dots, x_n^k$. Process $a_i$ can write in its own memory cell $x_i^k$, but it is allowed to read all memory cells. In this model, each process $a_i$ does the following, at round $k$:

* Process $a_i$ writes its current local state in the shared array: $x_i^k \leftarrow v_i$.

* It then takes a snapshot of the entire memory, reading the current values of $x_1^k, \dots, x_n^k$.

* Then, it performs some local computation to update its local state according to the values observed in the round: $v_i \leftarrow f(v_i, x_1^k, \dots, x_n^k)$, for some computable function $f$.

All processes perform these steps asynchronously, for each round from 1, ..., $k$. A protocol is called *full-information* when the local computation in the third step simply consists in storing the entire array $x_1^k, \dots, x_n^k$ that has been read. An execution is called *immediate* when the first two steps

<footnote n="1">¹$F_!$ is unique since all elements of $B^{\text{op}}\mathbf{Set}$ are direct limits of representable functors, i.e. of the form $B[b]$.</footnote>
(write and snapshot) never occur too far apart from each other. More precisely, whenever a process takes a snapshots, all processes with pending writes must also take a snapshot before another write can occur. This immediacy condition somewhat breaks the asynchrony assumption; but this behavior can actually be simulated in a fully asynchronous setting [27].

In our setting, the full-information immediate snapshot protocol can be formally defined by the following functor $G : \Gamma \to \Gamma^{\text{op}}\text{Set}$. For $A \in \Gamma$ a set of active processes, we define a chromatic simplicial set (in fact, it happens to be a simplicial complex) $G(A) \in \Gamma^{\text{op}}\text{Set}$ as follows. The vertices of $G(A)$ are pairs of the form $(b_i, V_i)$, where $b_i$ is a participating process, and $V_i$ is the view of $b_i$, that is, the set of processes whose value was read by $b_i$. The $B$-simplices of $G(A)$ are compatible sets of such vertices. Formally, if $B \subsetneq A$, we let $G(A)(B) = \emptyset$. Otherwise, let us write $B = \{b_0, \dots, b_m\} \subseteq A$, and define the set of $B$-colored simplexes of $G(A)$:

$$ G(A)(B) = \left\{ \{(b_0, V_0), \dots, (b_m, V_m)\} \left| \begin{array}{l} V_i \subseteq A \\ \forall i, 0 \le i \le m, b_i \in V_i \\ \forall i, j, 0 \le i, j \le m, (V_i \subseteq V_j) \text{ or } (V_j \subseteq V_i) \\ \forall i, j, 0 \le i, j \le m, a_i \in V_j \implies V_i \subseteq V_j \end{array} \right. \right\} \quad (2) $$

(see e.g. [28] or [29] for why those particular conditions on the views $V_i$ work). To complete the definition of the simplicial set $G(A)$, we also need to define the face maps: for $B' \subseteq B$,

$$ G(A)(\delta_{B',B}) : \begin{array}{ccc} G(A)(B) & \to & G(A)(B') \\ \{(b_0, V_0), \dots, (b_m, V_m)\} & \mapsto & \{(b_i, V_i) \mid b_i \in B'\} \end{array} $$

This defines the functor $G$ on the objects of $\Gamma$. Finally, the action of $G$ on the inclusion maps $\delta_{A',A}$ is given by:

$$ G(\delta_{A',A})(B) : \begin{array}{ccc} G(A')(B) & \to & G(A)(B) \\ \{(b_0, V_0), \dots, (b_m, V_m)\} & \mapsto & \{(b_0, V_0), \dots, (b_m, V_m)\} \end{array} $$

which is well-defined because if $V_i \subseteq A'$ and $A' \subseteq A$, then $V_i \subseteq A$.

This completes the definition of the functor $G : \Gamma \to \Gamma^{\text{op}}\text{Set}$, which describes the protocol complex of the immediate snapshot protocol for one round and one initial state. From Lemma 4.1, we get a functor $G_! : \Gamma^{\text{op}}\text{Set} \to \Gamma^{\text{op}}\text{Set}$, which describes the one-round protocol complex for any input complex. Intuitively, what the functor $G_!$ does is the following: for every simplex of the input complex, whose set of participating processes is $U \subseteq A$, we take one copy of $G(U)$; and then those copies are glued together according to the face maps of the input complex.

**Example 4.2.** Below is depicted the complex $G(A)$, where the set of processes is $A = \{a, b, c\}$ (also represented as colors blue, red, green, respectively). The complex $G(A)$ consists of 12 vertices labeled $v_0, \dots, v_{11}$, and the encoding of Equation (2) for each vertex is given next to the picture. The 13 triangles correspond to the 13 sets of compatible vertices respecting the conditions of Equation (2); they also correspond to the 13 executions of the immediate snapshot protocol for three processes.
Let $A' = \{a, b\} \subseteq A$. The simplicial complex $G(A')$ can also be seen in the picture, as the sub-complex of $G(A)$ consisting of the four vertices $v_0, v_1, v_6, v_8$, together with the three edges between them. The morphism of csets $G(\delta_{A',A}) : G(A') \to G(A)$ is the inclusion of $G(A')$ into $G(A)$.

<figure><img src="image_8.png" /></figure>

$v_0 = (a, \{a\})$

$v_6 = (a, \{a, b\})$

$v_1 = (b, \{b\})$

$v_7 = (a, \{a, c\})$

$v_2 = (c, \{c\})$

$v_8 = (b, \{a, b\})$

$v_3 = (a, \{a, b, c\})$

$v_9 = (b, \{b, c\})$

$v_4 = (b, \{a, b, c\})$

$v_{10} = (c, \{a, c\})$

$v_5 = (c, \{a, b, c\})$

$v_{11} = (c, \{b, c\})$

**4.3. A more general class of examples: dynamic networks**

The immediate snapshot example is an instance of a more general framework, called *dynamic networks* [30], also studied in the setting of epistemic logic using the so-called *communication pattern models* [31]. Here, we describe the special case of dynamic networks with *oblivious adversary* [32], meaning that the set of possible communication graphs is the same at each round. A hint of a potential generalization is given in Section 8 and Example 8.3. Moreover, we model crash failures explicitly by using the lack of reflexive edge in a communication graph to mean that the corresponding agent had crashed during the current round of communication.

**Definition 4.3. (Communication graph)**

Given a finite set of agents $A$, a *communication graph* on $A$ is a (directed) graph $G \subseteq A \times A$. When $G$ is clear from context, we write $a \to b$ instead of $(a, b) \in G$. We say that agent $a$ is *active* in $G$ when $a \to a$, and that $a$ has *crashed* otherwise. The *view* of an active agent $a$ in $G$ is $\text{view}_G(a) = \{b \in A \mid b \to a\}$. The view is undefined for crashed agents.

Intuitively, a communication graph describes a round of communication between the currently active agents. An edge $a \to b$ indicates that agent $a$ successfully sent a message to agent $b$. Reflexive edges indicate whether an agent has crashed during the current round, or is still active: crashed agents will not participate in subsequent rounds.

**Definition 4.4. (Dynamic network model)**

Given a finite set of agents $A$, an *oblivious message adversary* for $A$ is a set of communication graphs on $A$. A *dynamic network model* is a family $(M_U)_{U \subseteq A}$, where for each subset $U \subseteq A$, $M_U$ is an *oblivious message adversary* for $U$.

An *oblivious message adversary* specifies a set of possible communicative events that may occur at each round. For instance, if we want to specify that at most one message may be lost at each round,
the corresponding adversary is the set of all communication graphs where at most one edge is missing.

On the other hand, a dynamic network model specifies an oblivious message adversary for each
possible subset of the participating agents. This allows us to model, for example, a situation where at
most one agent may crash at each round of computation. If a agent crashes during the first round, then
in the second round we use the message adversary that concerns only the agent that are still active.

It may seem cumbersome to specify a message adversary $M_U$ for every possible subset of agents $U \subseteq A$. Indeed, most protocols considered in practice behave “uniformly”, meaning that the set of possible behaviors does not depend on the set of participating agents. In such a case, one can specify the adversary $M_A$ for the set of all agents; and then the family $(M_U)$ can be defined canonically by $M_U = \{G \upharpoonright_U G \in M_A\}$, where $G \upharpoonright_U$ denotes the induced subgraph of $G$ restricted to the set of vertices $U$. Not all protocols behave like this however: a counter-example is given by so-called *k-resilient protocols*, where at most *k* agents may crash during the execution of the system. To model this, the message adversary $M_U$ allows crashes to occur only when $\#(A \setminus U) \le k$.

**Full-information protocol complex for dynamic networks.** Let $A$ be a finite set of agents, and let us fix a dynamic network model $(M_U)_{U \subseteq A}$. We describe the corresponding full-information protocol complex as a functor $F : \Gamma \to \Gamma^{\text{opSet}}$.

With an object $U \subseteq A$ of $\Gamma$, we associate a cset, defined as a functor $F(U) : \Gamma^{\text{op}} \to \text{Set}$. For $V \subseteq A$, we define $F(U)(V)$ the set of $V$-colored simplexes of the cset $F(U)$.

$$
\begin{array}{l@{\qquad}l}
F(U)(V) = \emptyset & \text{if } V \not\subseteq U \\
F(U)(V) = \{(v, \text{view}_G(v)) \mid v \in V\} \mid G \in M_{U'} \text{ for some } U' \subseteq U, \text{ and } V \subseteq \text{active}(G)\} & \text{otherwise}
\end{array}
$$

To get a functor $F(U) : \Gamma^{\text{op}} \to \mathbf{Set}$, we also need to define the face maps: if $V \subseteq W$, we define

$$
\begin{array}{ccc}
F(U)(\delta_{V,W}) : F(U)(W) & \to & F(U)(V) \\
\{(v, \text{view}_G(W)) \mid w \in W\} & \mapsto & \{(v, \text{view}_G(V)) \mid v \in V\}
\end{array}
$$

which is well-defined since whenever $W \subseteq \text{active}(G)$, we also have $V \subseteq W \subseteq \text{active}(G)$.

Finally, $F$ itself needs to be a functor from $\Gamma$ to $\Gamma^{\text{opSet}}$, so for $U \subseteq T$ we need to define a
morphism of simplicial sets $F(\delta_{U,T}) : F(U) \to F(T)$. This morphism is given by the family of
functions:

$$
\begin{array}{ccc}
F(\delta_{U,T})(V) : F(U)(V) & \to & F(T)(V) \\
\{(v, \text{view}_G(v)) | v \in V\} & \mapsto & \{(v, \text{view}_G(v)) | v \in V\}
\end{array}
$$

which is well-defined, because the communication graph *G* is required to be in *M*<sub>*U*</sub> for some *U*'<sub>\*\*</sub> *subseteq U*;
but then we can still pick the same *G* since *U*'<sub>\*\*</sub> *subseteq* *U*<sub>\*\*</sub> *subseteq* *T*.

**Example 4.5. (Reliable broadcast)**

Let us start with a very simple and slightly degenerate example, that illustrates some of the subtleties
in our definition of the protocol complex. We consider a reliable broadcast, with no crashes or missed
messages. This can be modeled as a dynamic network model, by taking for every $U \subseteq A$ the oblivious
message adversary $M_U = \{K_U\}$, where $K_U$ denotes the complete graph on the set of vertices $U$.
One might expect the protocol complex functor to send a set $U \subseteq A$ of agents to a single simplex, since there is only one possible execution; but this is not the case. Indeed, in the definition of the simplicial complex $F(U)$, we have to choose a subset $U' \subseteq U$ of participating agents. Then, we (reliably) broadcast messages among this set $U'$ of agents, and collect their views. So, in fact, we get one maximal simplex for each subset $U' \subseteq U$. This detail is crucial to be able to define the functorial action $F(\delta_{U,T})$, which tells us how the functor $F_!$ will “glue together” the various components of the protocol complex.

The figure below depicts simplicial complexes $F(\{a, b\})$ and $F(\{a, b, c\})$ for the reliable broadcast protocol. On the picture, only the names of the agents $(a, b, \text{or } c)$ are written; not their views. Since $\{a, b\} \subseteq \{a, b, c\}$, we have a morphism $F(\delta_{\{a,b\}, \{a,b,c\}}) : F(\{a, b\}) \to F(\{a, b, c\})$, which is the obvious inclusion.

<figure><img src="image_9.png" /></figure>

**Example 4.6. (Immediate snapshot, revisited)**

Let us consider again the immediate snapshot protocol of Example 4.2, seen as a dynamic network model. First, we need to define the possible communication graphs for any set $U$ of participating agents. Define an *ordered partition* of $U$ to be a sequence of subsets $S = (S_1, \dots, S_k)$, such that $\cup_i S_i = U$ and $S_i \cap S_j = \emptyset$ for all $i \neq j$. The communication graph $G_S$ associated with an ordered partition has an edge $a \to b$ (for $a, b \in U$) whenever $a \in S_i$ and $b \in S_j$ with $i \le j$.

$$M_U = \{G_S \mid S \text{ is an ordered partition of } U\}$$

This defines the immediate snapshot protocol as a dynamic network model. For example, for a set of three agents $U = \{a, b, c\}$, the above definition yields a total of 13 graphs, corresponding to the 13 ordered partitions of $\{a, b, c\}$. Four graphs are depicted below, with the corresponding ordered partition written under it. All other graphs can be obtained by switching the roles of $a, b$ and $c$.

<figure><img src="image_10.png" /></figure>
Note that this model does not allow crash failures; so all agents are active in all communication graphs. It can be checked that the protocol complex functor associated with this dynamic network model is the same one as the functor given in Example 4.2. Indeed, the four conditions on the sets $V_0, \dots, V_m$ that appear in Equation (2) characterize exactly the set of views associated with an ordered partition, as well known from [1].

**Example 4.7. (Synchronous broadcast with crash failures)**

Let us consider now agents communicating though asynchronous message-passing. In this model, each agent $P_i$ (among a set of agents $P_k$, $k = 0, \dots, n$) does the following, at each round,

• it broadcasts the value contained in its output buffer, $x_i^i$, to all other agents, by a succession of sends, in no definite order,

• it stores data that has reached it from another agent, into its input buffer. The input buffer is composed of locations $x_j^i, j = 1, \dots, \hat{i}, \dots, n$ in which $P_i$ stores the value it received in the same round from $P_j$. Notice that the input and output buffer form together an array of $n + 1$ locations, $x_k^i, k = 0, \dots, n$.

• it then performs some local computation, basically amounting to the calculation of some partial recursive function $f$ on the values of some local variables $y_1, \dots, y_l$ and the assignment of the result to a local variable $x$.

The full-information complex corresponding to this model is again the one where the local computation part is replaced by the history of communication. This comes directly from the formalization of this distributed architecture using communication patterns.

Consider for instance the set of agents $A = \{a, b, c\}$ and the following communication graphs on $A$:

<figure><img src="image_11.png" /></figure>

We name these graphs $G_1, \dots, G_4$, from left to right. Note that we omitted some graphs that can be obtained from those by permuting the names of the agents (i.e., graphs where agent $b$ or $c$ crashed instead of $a$). Intuitively,

• $G_1$ is an execution where no crash occurred, all messages were successfully delivered;

• $G_2, G_3, G_4$ are executions where only agent $a$ crashed, after sending 0, 1 or 2 messages.

Among those communication graphs, only $G_1, G_2$ and $G_3$ have “detectable crashes”, in the sense that whenever a agent is crashed, at least one of the remaining agents knows about it (because no message was received from the crashed agent). So let us define two communication patterns: $P_{\text{detectable}}$ contains $G_1, G_2, G_3$ as well as graphs obtained from them by permuting the names of the agents (totalling 10 graphs); and $P_{\text{undetectable}}$ contains $G_1, G_2, G_3, G_4$ as well as permutations of them (totalling 13 graphs).
Suppose we start with an initial chromatic semi-simplicial set $C'$ with two triangles $w$ and $w'$ that are glued along their *bc*-coloured edge. In the case of undetectable crashes, we get the simplicial complex depicted on the right, with 19 worlds named $w_0, \dots, w_9$ and $w'_0, \dots, w'_9$ (notice that $w'_5$ is missing).

<figure><img src="image_12.png" /></figure>

$C'$

<figure><img src="image_13.png" /></figure>

One step synchronous broadcast from $C'$

For instance, the world labelled $w_5$ corresponds to both the effect of graph $G_2$ on $w$ and $w'$ at the same time. Indeed, when the communication graph $G_2$ occurs, $a$ has crashed and the two agents $b$ and $c$ exchange information. But neither $b$ nor $c$ is able to distinguish between the initial worlds $w$ and $w'$. So no matter whether we started in $w$ or $w'$, the two remaining agents end up with the same local state.

# 5. Protocol complex algebras and co-algebras

## 5.1. Algebras induced by protocols

There is a last ingredient which will prove useful in the discussion of temporal-epistemic logics. In full-information protocol complexes, local states of agents are obtained as a pair of local initial state and of the full history of communication. This means that there is a projection operator, to the first component, from $F_!(X)$ to $X$, for any cset $X$ as we see below for round-based oblivious protocols:

**Proposition 5.1.** The full information protocol complex for any pattern of communication naturally comes with an algebra $F(X) \to X$.

**Proof:**

Let $U \in \Gamma$, we prove first that $F$ seen as a functor from $\Gamma$ to $\Gamma^{\text{OP}} \to \text{Set}$, is such that there is a map from $F(U)$ to $\Gamma[U]$, the cset which has generated by a unique $U$-simplex. The result will hold by taking colimits over the chromatic simplexes of any $X \in \Gamma^{\text{OP}}\text{Set}$ with the Yoneda extension of $F$.

For all $V \subseteq U$, we define the map $f_U$ of cset, such that $f_U(V)$, $V \subseteq U$ from $F(U)(V)$ to $\Gamma(V, U)$ is defined as follows. To each set $\{(v, \text{view}_G(v)) \mid v \in V\}$ for some $G \in M_{U'}$ ($U' \subseteq U$ and $V \subseteq \text{active}(G)$) we associate indeed the only $V$ simplex of $\Gamma[U]$, which is the inclusion of $V$ into $U$. It is easy to check that $f$ defines a morphism in $\Gamma^{\text{OP}}\text{Set}$ since $f_U(V)$ is a sub-chromatic simplex of $f_U(W)$ in $\Gamma[U]$, for $V \subseteq W \subseteq U$. $\square$
**Example 5.2. (Synchronous broadcast case)**

In the case of the synchronous broadcast of Example 4.7 from the simplicial set with two triangles, the corresponding algebra map is as follows. Triangles $w_0$ and $w'_0$ are mapped onto $w$ and $w'$ respectively. Call $w_{ab}$, $w_{bc}$, $w_{ac}$ (resp. $w'_{ab}$, $w'_{bc}$, $w'_{ac}$) the ab, bc, ca 1-simplex boundary of $w_0$ (resp. of $w'$), the algebra map associates $w_1$, $w_2$, $w_3$ (resp. $w'_1$, $w'_2$, $w'_3$) on $w_{a,b}$ (resp. on $w'_{a,b}$); $w_7$, $w_8$, $w_9$ (resp. $w'_7$, $w'_8$, $w'_9$) on $w_{a,c}$ (resp. $w'_{a,c}$); $w_4$, $w_5$, $w_6$ (resp. $w'_4$, $w'_5$, $w'_6$) on $w_{b,c}$ (resp. $w'_{b,c}$).

As we can see in the example above, this natural algebra map sends states in the protocol complex from some input cset $I$ (i.e. states after one round of communication) to the states they originated from within $I$.

**5.2. The co-algebraic view**

Co-algebras are the dual of algebras, as shown in the definition below. Modal logics are known to be related to $G$-co-algebras in the literature, see e.g. [33].

**Definition 5.3. (G-coalgebra)**

Let $G$ be an endofunctor, $G : D \to D$. A $G$-coalgebra is a pair $(D, c : D \to G(D))$ where $D \in D$. Let $(D, c)$ and $(D', c')$ be two $G$-coalgebras. Then $g$ is a morphism of $G$-algebras from $(D, c)$ to $(D', c')$ if and only $g$ is a morphism from $D$ to $D'$ in $D$ and the following diagram commutes:

<figure><img src="image_14.png" /></figure>

We write $coAlg(G)$ for the category of $G$-coalgebras.

A non-deterministic transition system naturally gives rise to an co-algebra over a certain (fixed) endofunctor on sets. Similarly to Section 2, given a set $Ac$ of “actions” (or labels), consider an endofunctor $F$ on sets $X \mapsto \wp(X \times Ac)$. Then, a (set-theoretic) map $A : X \to \wp(X \times Ac)$ can be seen as a non-deterministic automaton: indeed, given $x \in X$, where $x$ is seen as a state, the function $A$ assigns to $x$ a set of pairs $(y, a)$ made up of an action $a$ and a state $y$, to be interpreted as the states $y$ that can be reached from $a$ by firing action $a$.

From a given $F$-algebra, there is a simple, and bi-univoque way to generate a $G$-algebra, when $G$ is right-adjoint to $F$ as we see below:

**Lemma 5.4.** Suppose that $F : C \to C$ is left adjoint to functor $G : C \to C$. Then the category of $F$-algebras is isomorphic to the category of $G$-coalgebras.

**Proof:**

Take $(C, a : F(C) \to C)$ a $F$-algebra and consider the composite of $G(a)$ with the unit $\epsilon_C$ on $C$ of the adjunction:
$$C \xrightarrow{\epsilon_C} GF(C) \xrightarrow{G(a)} G(C)$$

This defines a G-coalgebra. Inversely, take $(D, c : D \to G(D))$ a G-coalgebra and consider the composite of $F(c)$ with the counit $\epsilon_C$ on $C$ of the adjunction:

$$F(D) \xrightarrow{F(c)} FG(D) \xrightarrow{\eta_D} D$$

is a F-algebra on $D$. The fact that these two operations are inverse from one another is a direct consequence of the axioms on units and counits of adjunctions. $\square$

But indeed, the G-algebra corresponding through Lemma 5.4 to the F-algebra of deterministic automata, Section 2 is not the one, of non-deterministic automata, that we mentionned in the beginning of this Section. We recall that deterministic automata are F-algebras for functor $F$ associating to each set $X$, the set $X \times Ac$. The right-adjoint to $F$ is $G$ associating to each set $X$, the set of functions from $Ac$ to $X$. Indeed G-algebras are just another encoding of deterministic automata. A map from $X$ to $G(X)$ is just a map which associates to each state $x$ and action $a$, a “next” state $y$.

In the situation of full-information protocol complex functors, we have naturally a right-adjoint $F^*$ to the protocol complex functor $F_1$. So $F_1$-algebras correspond to $F^*$-coalgebras. In some sense, the $F_1$-algebras we have are really similar to the encoding of deterministic transition systems, but in theory $F^*$-coalgebras should be more “powerful” and also could deal with even non-bounded non-deterministic transition systems.

This co-algebraic view of protocol complex functors are in relation with the classical “carrier map” view of protocols, as we show below in a particular case.

By Lemma 4.1, the G-coalgebras that correspond to our F-algebras implementing protocol complexes, are defined by $G(X) = \Gamma^{\text{op}}\text{Set}(F(.), X)$ meaning that the $\gamma$ simplices of $G(X)$, for $\gamma \in \Gamma$, $G(X)(\gamma)$ is the set of maps from $F(\gamma)$ to $X$. Now, a G-coalgebra is a map in $\Gamma^{\text{op}}\text{Set}$ from $X$ to $G(X)$. This maps to any $\gamma$-simplex of $X$, a map from $F(\gamma)$ to $X$. This map from $F(\gamma)$ to $X$ corresponds to the carrier map applied to the set of participating processing $\gamma \in \Gamma$ of [1].

# 6. Iterated protocol complexes and free algebras

We now note that:

**Lemma 6.1.** Let $F : \Gamma \to \Gamma^{\text{op}}\text{Set}$ be a functor that sends inclusion maps $A \hookrightarrow B$ of elements $A$, $B$ of $\Gamma$ to inclusions of csets $F(A) \hookrightarrow F(B)$. Then its left Yoneda extension $F_1$ preserves monomorphisms.

**Proof:**

As well known, [34] (and [35] for the more general case), left Kan extensions $F_1$ of a functor $F : C \to \mathcal{E}$ preserve all colimits as left adjoints, and any finite limit when $F$ preserves these finite limits, at least in the case when $\mathcal{E}$ is a topos. This is the case here where $C = \mathcal{E} = \Gamma^{\text{op}}\text{Set}$. Indeed, as well-known as well, monomorphisms are morphisms obeying a certain pullback diagram, hence if $F$ preserves monomorphisms, $F_1$ preserves monomorphisms as well. Finally, monomorphisms in $\Gamma$ and in $\Gamma^{\text{op}}\text{Set}$ are inclusion maps. $\square$
It is clear that for distributed applications, $F(B)$ is going to contain as a subcomplex $F(A)$ where $A$ is a subset of agents of $B$. We particularize this to well-known protocol complex examples for a start:

**Example 6.2.** We have already noted in Example 4.2, $G$ corresponding to the immediate snapshot model, preserve inclusion maps $\delta_{U,V}$. By Lemma 6.1, $G_!$ preserve monomorphisms. As it is a left adjoint, it also preserves colimits.

For general patterns of communication, we have the same phenomenon:

**Lemma 6.3.** The protocol complex functors for general patterns of communication (Section 4) defines a functor $F_! : \Gamma^{\text{op}}\mathbf{Set} \to \Gamma^{\text{op}}\mathbf{Set}$ that preserves colimits and monomorphisms.

**Proof:**

As protocol complexes defined in Section 4 are defined by Yoneda extensions, they preserve colimits, as they are left-adjoints, see Lemma 4.1.

Now, we observe that the protocol complex functors defined in Section 4 are such that $F(\delta_{U,T})$ is a monomorphism, as this defines an inclusion of the set of $V$-simplexes of $F(U)$ into the set of $V$-simplexes of $F(T)$. The result is then a consequence of Lemma 6.1. $\square$

The dynamics of a distributed system in the framework of e.g. [1] is given by the iteration of the protocol complex functor. The natural question is how to wrap up formally all the iterations of the protocol complex. The right formalization is given through the notion of free algebra as we know. Now, thanks to Theorem 2.4, Lemma 6.1 and Lemma 6.3, we know that in our general case where our protocol complex satisfies Hypotheses (1) to (4), we know that they provide us with varietors, and that we have a general Kleene-like formula for the free algebra generated by a given cset.

# 7. Temporal-epistemic logics on free algebras

In this section, we develop a temporal-epistemic logics which has a natural semantics in terms of chromatic simplicial sets, and which will be adapted to specifying and verifying the diverse protocols we have been modelling in the previous sections.

## 7.1. The logics

In this section, we are going to consider the following modal logics, extending first-order predicate logics on a given set $At$ of atomic predicates:

$$ \phi ::= p \mid \neg p \mid \phi \lor \phi \mid K_a\phi \mid C_B\phi \mid D_B\phi \mid X\phi \mid \Box\phi \mid \Diamond\phi $$

where $p \in At$, $K_a\phi$ reads “agent $a$ knows $\phi$”, $C_B\phi$ means “subgroup $B$ of agents have the common knowledge of $\phi$”, $D_B\phi$ means “subgroup $B$ of agents have distributed knowledge of $\phi$”, $X\phi$ read “next $\phi$”, resp. $\Box\phi$, “always $\phi$” and $\Diamond\phi$, “eventually $\phi$”.

We consider also the following predicates, that will reveal convenient in the sequel:
$$
\text{dead}(a) := K_a \text{false}
$$

$$
\text{dead}(U) := \bigwedge_{a \in U} \text{dead}(a)
$$

$$
\text{alive}(a) := \hat{K}_a \text{true}
$$

$$
\text{alive}(U) := \hat{D}_U \text{true}
$$

As already used in [36], dead(a) precisely models the fact that an agent is crashed in some world, as being equivalent to the fact it knows “false”. Properties alive(a), dead(U) and alive(U) are all derived from this.

7.2. Chromatic augmented semi-simplicial sets as simplicial models

In this section, we give a semantics of the logics of Section 7.1 based on the “maximal epistemic covering model” of [13] (also similar to the maximal simplicial complex models of [37]). In these maximal models, all simplexes, of any dimension, are worlds in the sense of the more classical Kripke semantics. We also suppose we have a locality axiom, that is, At is partitionned into At<sub>a</sub>, for a ∈ A, sets of “local atomic predicates” for agent a.

**Definition 7.1. (Semi-simplicial model)**

A semi-simplicial model $X = \langle S, \ell \rangle$ consists of a chromatic semi-simplicial set $S$, together with a labelling $\ell : S_0 \to \mathcal{P}(\text{At})$ that associates with each vertex $s$ of $S$ a set of atomic propositions $\ell(s) \subseteq \text{At}_{\chi(s)}$ that hold there. A morphism of semi-simplicial models $\alpha : X \to Y$ is a morphism of chromatic semi-simplicial models that does not create new labelling: $\ell'(\alpha(s)) \subseteq \ell(s)$. We denote by $cset_{\text{At}}$ the category of semi-simplicial models.

Note that for any semi-simplicial model $\langle S, \ell \rangle$, the labelling function $\ell$ can be extended to a function, still written $\ell$ from all simplexes of $S$ to $\mathcal{P}(\text{At})$ by, for $w \in S_n$ a $n$-simplex ($n \ge 0$),

$$
\ell(w) = \bigcup_{0 \le i_1 < i_2 < \dots < i_n \le n} \{ \ell(d_{i_1} \circ d_{i_2} \circ \dots \circ d_{i_n}(w)) \} \quad (3)
$$

Indeed, the notions of algebra, coalgebra and free algebra lift to category $cset_{\text{At}}$.

It is also straightforward to extend the cset description of the protocol complex functor for all
patterns of communication to a functor from $cset_{\text{At}}$ to $cset_{\text{At}}$. Given a simplex $s$ of a $cset_{\text{At}}$ $X = \langle S, \ell \rangle$
with vertices $s_0, \dots, s_m$, we produce the cset $F(s)$ for a given pattern of communication, and a $cset_{\text{At}}$
that we denote also by $F(s)$, where all vertices $v$ of $F(s)$ have associated predicate $\ell(s_{\chi(v)})$. This
means that we just copy the predicates defining the “initial value” of the corresponding agent, to the
vertices in the image of $F$.

**7.3. Semantics in free algebras over chromatic simplicial sets**

The semantics of the temporal-epistemic logics we are considering can be given in any object $I^\infty$ of
the free $F$-algebra over some element $I \in cset_{\text{At}}$, given an algebra $q : F(I) \to I$, as we will see now.

We note $\lnk_a(x, y)$ (resp. $\lnk_B(x, y)$), for $x, y \in C$, $C$ a given cset, for the following predicate.
We have $\lnk_a(x, y)$ to be true iff there is an inclusion map $i$ from $\Gamma^{\text{op}}\mathbf{Set}[a]$ (resp. $\Gamma^{\text{op}}\mathbf{Set}[B]$) to $C$
with the image of *i* included in both *x* and *y*. Geometrically speaking, $lnk_a(x, y)$ is true iff *x* and *y* share a *a* (resp. *B*) simplex in *C*.

Our semantics takes the following form:

(At) $I^{\infty}, x \models p$ iff $p \in \ell(x)$

(Neg) $I^{\infty}, x \models \neg \varphi$ iff $I^{\infty}, x \not\models \varphi$

(And) $I^{\infty}, x \models \varphi \wedge \psi$ iff $I^{\infty}, x \models \varphi$ and $I^{\infty}, x \models \psi$

(K) $I^{\infty}, x \models K_a \varphi$ iff for all $y \in I^{\infty}, lnk_a(x, y)$ implies $I^{\infty}, y \models \varphi$

(C) $I^{\infty}, x \models C_B \varphi$ iff for all $y \in I^{\infty}, y = y_n, lnk_B(y_i \cap y_{i-1}), i = 1, \dots, n,$
$y_1 = x$ implies $I^{\infty}, y \models \varphi$

(D) $I^{\infty}, x \models D_B \varphi$ iff for all $y \in I^{\infty}, lnk_B(x, y)$ implies $I^{\infty}, y \models \varphi$

(X) $I^{\infty}, x \models X \varphi$ iff for all $y \in F^{n+1}(I)$, $n$ s.t. $x \in F^n(I)$, $F^n(q)(y) = x$
implies $I^{\infty}, y \models \varphi$

(Box) $I^{\infty}, x \models \Box \varphi$ iff for all $i \ge 0, I^{\infty}, x \models X^i \varphi$

(Diam) $I^{\infty}, x \models \Diamond \varphi$ iff exists $i \ge 0, I^{\infty}, x \models X^i \varphi$

This reads as follows:

* (At), (Neg), (And) give the obvious semantics of the underlying first-order logic

* (K) is the interpretation of the knowledge modal operator of [13]: agent *a* knows $\varphi$ in world *x* if $\varphi$ is true in all worlds *y* that are connected to world *x* through vertex *a* of *x*.

* (C) and (D) are similar to [13] as well: the group *B* of agents has common knowledge of $\varphi$ in world *x* if $\varphi$ is true on all worlds *y* that are reachable from a path of worlds that are connected to *x* by vertices labelled by *B*. And *B* has distributed knowledge in world *x* of $\varphi$ if $\varphi$ is true in all worlds *y* that are connected to *x* through vertices in *B* of *x*.

* Equation (X) defines the semantics of the temporal modality “next step” and reads as follows: $\varphi$ is true after one step from world *x*, which is in $I^{\infty}$ hence in $F^n(I)$ for some $n \in \mathbb{N}$, which is necessarily unique (since $I^{\infty}$ is the infinite coproduct of all the $F^n(I)$, $n \in \mathbb{N}$, by Theorem 2.4) if $\varphi$ is true in all worlds *y* in the chromatic simplicial set in the next step $F^{n+1}(I)$, which are possible next steps of *x*. The interpretation of the “always” (Box) and “eventually” (Diam) temporal modalities are then obvious.

Note that simplicial models generate history LTS in the sense of [10]. The latter structures are defined as the unfolding of transition systems together with an indistinguishability (equivalence) relations on states (one per agent), in such a way that the equivalence naturally lifts to histories. Indeed, our free algebra model is a history based model, where the states are all simplexes, and the indistinguishability relation for an agent *a* between two states *x* and *y* is given by $lnk_a(x \cap y)$. The gain we are making with our modelling is, apart from a clean categorical construction, the use of geometric properties of the state space (modeled by simplicial sets), for proving or disproving the existence of tasks that verify some specification.

Note also that in the particular case of the immediate snapshot model (Example 4.2), the Dynamic Epistemic Logic (DEL) framework of [14] is a fragment of the logic we give in this section: rule (X)
given for “next $\varphi$” indeed reflects the effect of the update or public announcement that is made in the
corresponding action model, on the validity of formula $\varphi$.

**7.4. Axiomatics**

First, we note that we have an analogous of the “knowledge gain” theorem of [11]. This will allow
us in particular to derive some sound axioms that relate the temporal modalities with the epistemic
modalities.

An epistemic logic formula $\phi \in \mathcal{L}_K$ is called *positive* when it does not contain negations, except possibly in front of atomic propositions. Formally, positive formulas are built according to the following grammar:

$$ \varphi ::= p \mid \neg p \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid K_a \varphi \mid C_B \varphi \mid D_B \varphi \quad a \in A, p \in \text{At} $$

We write $\mathcal{L}_K^+$ for the set of positive epistemic formulas. Essentially, positive formulas forbid talking about what an agent does not know.

**Theorem 7.2. (knowledge gain)**

Consider simplicial models $C = \langle S, \ell \rangle$ and $\mathcal{D} = \langle S', \ell' \rangle$, and a morphism of pointed simplicial models $f : (C, w) \to (\mathcal{D}, w')$. Let $\varphi \in \mathcal{L}_K^+$ be a positive formula. Then $\mathcal{D}, w' \models \varphi$ implies $C, w \models \varphi$.

**Proof:**

We proceed by induction on the structure of the (positive) formula $\varphi$. For the base case $\varphi = p \in \text{At}$, as $\mathcal{D}, w' \models p$ we know that $p \in \ell'(w')$. But as $f$ is a morphism of semi-simplicial models and $f(w) = w'$, this implies that $\ell'(w') = \ell'(f(w)) \subseteq \ell(w)$. Thus, $p \in \ell(w)$ and $\mathcal{D}, w \models \varphi$.

A similar reasoning works in the case of a negated atomic proposition $\neg p$. The cases of conjunction and disjunction follow trivially from the induction hypothesis.

Suppose now that $\mathcal{D}, w' \models K_a \varphi$. There are two cases: there is no $a$-colored vertex in $w'$, therefore, as $w' = f(w)$, there is no $a$-colored vertex in $w$ either, therefore it also trivially holds that $\mathcal{D}, w \models K_a \varphi$. The other case is that there is an $a$-colored vertex in $w'$, and $w$. Suppose now that $\text{lnk}_a(w, z)$ for some facet $z$ of $C$, and let us prove that $C, z \models \varphi$. Let $v$ be an $a$-coloured vertex common to $z$ and $w$. Then $f(v)$ is an $a$-coloured vertex in both $f(z)$ and $f(w)$. And because $\mathcal{D}, w' \models K_a \varphi$, $\mathcal{D}, f(z) \models \varphi$ and by induction on the formula, $C, z \models \varphi$.

The rest follows easily for the other connectives. $\square$

This now has the following consequence on the interpretation of our temporal epistemic logics as
defined in Section 8.3, for free algebras over chromatic simplicial sets:

**Lemma 7.3.** For any algebra $q : F(Q) \to Q$ and $\varphi$ any positive epistemic formula, we have, for $x \in F^n(Q)$:

$$ Q^\infty, x \models \varphi \Rightarrow Q^\infty, x \models X\varphi $$

and similarly, for $x \in F^n(Q)$:

$$ Q^\infty, x \models \varphi \Rightarrow Q^\infty, x \models \Box\varphi $$

$$ Q^\infty, x \models \varphi \Rightarrow Q^\infty, x \models \Diamond\varphi $$
**Proof:**

For $\varphi$ a positive formula, as $q : F(Q) \to Q$ is a morphism of simplicial models, we know by Theorem 7.2 that $Q, y \models \varphi$ implies $F(Q), x \models \varphi$ when $q(y) = x$. Similarly, $F^n(q) : F^{n+1}(Q) \to F^n(Q)$ is a morphism of simplicial models, so it holds as well that $F^n(Q), x \models \varphi$ implies $F^{n+1}(Q), y \models \varphi$ when $F^n(q)(y) = x$, i.e. $Q^\infty, x \models X\varphi$. By the semantics of $X\varphi$ this proves the first result.

For the second part, this is done by induction on the number of applications of $q$. Finally, we observe that $\Box\varphi$ implies $\diamond\varphi$. □

In particular, this means that our distributed machines never “forget” a true statement about the initial values of agents, that they may have learned through communication: they can only learn more, through communication.

On top of the axioms for normal modal logic, with all propositional tautologies, closure by modus ponens, and the necessitation rule, get the following set of sound axioms for our temporal-epistemic logics:

**Lemma 7.4.** The following axioms are sound in all free algebras over chromatic simplicial sets:

• (K) $D_U(\varphi \Rightarrow \psi) \Rightarrow (D_U\varphi \Rightarrow D_U\psi)$

• (4) $D_U\varphi \Rightarrow D_U D_U\varphi$

• (B) $\varphi \Rightarrow D_U \neg D_U \neg \varphi$

• (Mono) for $U \subseteq U'$, $D_U\varphi \Rightarrow D_{U'}\varphi$

• (Union) for $U, U'$, $\text{alive}(U) \wedge \text{alive}(U') \Rightarrow \text{alive}(U \cup U')$

• (NE) $\bigvee_{a \in A} \text{alive}(a)$;

• (P) $\text{alive}(U) \wedge \text{dead}(U^c) \wedge \varphi \Rightarrow D_U(\text{dead}(U^c) \Rightarrow \varphi)$;

• (Max) for $U \neq \emptyset$, $\text{alive}(U) \Rightarrow \neg D_U \neg \text{dead}(U^c)$;

• (GFP) $C_A(\varphi \implies \bigwedge_{a \in A} K_a\varphi) \implies (\varphi \implies C_A\varphi)$

• (KG) for $\varphi$ positive epistemic formula: $\varphi \Rightarrow X\varphi$

• (KG□) for $\varphi$ positive epistemic formula: $\varphi \Rightarrow \Box\varphi$

• (KG◇) for $\varphi$ positive epistemic formula: $\varphi \Rightarrow \Diamond\varphi$

• (AX) $\Box\varphi \Rightarrow X\Box\varphi$

• (XX) $\Box\varphi \Rightarrow \varphi$

• (AI) $\Box(\varphi \Rightarrow \psi) \Rightarrow \Box\varphi \Rightarrow \Box\psi$

• (E) $\Diamond\varphi \Leftrightarrow \neg\Box\neg\varphi$
**Proof:**

The first five axioms (K), (4), (B), (Mono) and (Union) are called KB4<sub>n</sub> + Mono + Union in [13] and are known to hold for the epistemic part of these csets.

The three following axioms (NE), (P) and (Max) hold because of Theorem 3 of [13]: the logic EC<sub>n</sub>+NE + P + Max is sound with respect to all chromatic semi-simplicial models.

Because of Theorem 7.2, we have also the following sound axioms: (KG), (KG□) and (KG◇).

We also check easily the classical axioms for temporal logics: (AX), (XX), (AI) and (E). For instance, suppose that $I^{\infty}, x \models \Box \varphi$. This means that for all $i \ge 0$, $I^i, x \models \varphi$, so in particular, $I, x \models \varphi$. Thus, $I^{\infty}, x \models (\Box \varphi \implies \varphi)$, for all models $I$ and $x \in I$. □

**7.5. Example: task specification in fault-tolerant distributed computing**

We slightly adapt the framework for task specification of [1], that we recapped in Section 3.1, to our framework, in which we use csets instead of chromatic simplicial complexes.

A task $\mathcal{T}$ is given by a cset of inputs $I$, a cset of outputs $O$, and a task specification $T$, a sub-cset of $I \times O$, the product of these two csets defined as follows: $(I \times O)_n = I_n \times O_n$ with $d_U(i, o) = (d_U(i), d_U(o))$. This cset $T$ relates inputs with potential outputs, that any protocol solving the task should choose from. Naturally, $T$ comes with a projection morphism $\pi_T : T \to I$.

Given a particular architecture of communication (dynamic network in our case, or pattern of communication), formalized by a protocol complex $P$ (or an iterated protocol complex) and the map $\pi_P$ relating worlds in $P$ (simplexes, or states) to worlds in the input complex $I$, we define solvability of a task $\mathcal{T}$ on this particular architecture as follows. Mathematically, task $\mathcal{T}$ is *solvable* using the protocol complex $P$ if there exists a cset morphism $\delta : P \to T$ such that $\pi_I \circ \delta = \pi_P$, i.e., the diagram of simplicial complexes below commutes.

<figure><img src="image_15.png" /></figure>

Our temporal-epistemic logics allows for more general task specifications in that we can specify the existence of such decision tasks at specific time instants (round numbers) during protocol execution.

For instance, for binary consensus, the atomic predicates in At<sub>i</sub> are equality predicates of their initial state with 0 or with 1 and the specification can be written in our temporal-epistemic logics as

$$ \diamond \left( C_A(\bigvee_{i \in A} p_i = 0) \wedge C_A(\bigvee_{i \in A} p_i = 1) \right) $$
**8. Beyond oblivious patterns of communication and generic protocols**

In this section, we discuss another presheaf model for distributed models which encodes protocols that can evolve according to non only participating values, but also local values of agents. The evolution of the system may depend on local decision values, and not just on the patterns of communication.

This model gives rise to a presheaf category, and the same machinery as the one used in the previous section can be used again, in particular, the definition of protocol functors through Yoneda extensions, algebras on these functors, and free algebras. We then discuss the strong connections that we may find between these approaches in Section 8.2.

Also, in the previous sections, we only considered "generic protocols" (full-information protocols in the case of e.g. the immediate snapshot model of Example 4.2); in Section 8.2, we show that protocol functors can only be defined for particular "interpreted protocols".

**8.1. Chromatic simplicial sets with decisions**

Let $\Psi$ be the category $\Gamma$ indexed by a category $\mathcal{V}$ of decision values. The objects of $\Psi$ are $(A, D)$ with $A \in \Gamma$ and $D : A \to \mathcal{V} \cup \{\perp\}$, a functor from the poset category $A$ to $\mathcal{V}$. Morphisms $f : (A, D) \to (B, E)$ are morphisms from $(A, D)$ to $(B, E)$ in $\Psi$.

**Definition 8.1. (Chromatic simplicial sets with decision values)**

We call the presheaf category $\Psi^{\text{op}}\text{Set}$ the category of chromatic simplicial sets with decision values.

Equivalently, by the fundamental theorem of topoi [34], objects of $\Psi^{\text{op}}\text{Set}$ can be seen as csets together with a labeling map to a chromatic simplicial set of possible decision values $\mathcal{O}$, defined as follows. Chromatic simplices $s$ (of dimension $m + 1$) of $\mathcal{O}$ are $s = ((a_0, d_0), \dots, (a_m, d_m))$ with $a_i \in \mathbb{N}$, $d_i \in \mathcal{V}$, satisfying $a_0 < \dots < a_m$. The color of $s$ is $(a_0, \dots, a_m)$ and the boundary operators are the obvious ones: $d_a(s) = ((a_0, d_0), \dots, (\widehat{a_i}, \widehat{d_i})), (a_m, d_m))$ when $a_i = a$. $\Psi^{\text{op}}\text{Set}$ is equivalent to $\Gamma^{\text{op}}\text{Set}/\mathcal{O}$, for $\Psi$ and $\mathcal{O}$ defined with the same $\mathcal{V}$.

This is the category in which we can describe protocols where each step may depend on local decision values, or an internal state such as a position, in distributed robotics:

**Example 8.2. (Distributed multi-robot systems)**

The task specification framework is also relevant for distributed systems that interact in the physical world, such as multi-robot systems. The distributed coordination of robots can be understood from the distributed computing perspective. The main model is that of luminous robots executing the look-compute-move (LCM) scheme [38], described next. Consider a set of robots $R_i$, $i = 1, \dots, n$, with positions $\mathbf{x}_i \in \mathbb{R}^p$ (for some $p \ge 1$). Each robot is equipped with a set of visible lights used for communication and memory. At each (global) step, they perform the following actions:

1. (look) They acquire the position and lights of the robots $R_j$, $j \neq i$, that are within their visibility radius $r$.

2. (compute) They compute their next move and new configuration of lights from what they observed.
3. (move) They update their new position and lights to the computed values.

We suppose that the dynamics of each robot is such that at each step, robot $R_i$ at current position $\mathbf{x}_i$ can only move to positions within a set $N_i(\mathbf{x}_i)$. Several properties of distributed systems are immediately translated, such as communication faults, synchronicity and limited interaction range<fnref n="2" />. In many ways this looks similar to the atomic snapshot model of Example 4.2, where the scan operation corresponds to “look”, and update corresponds to “compute-move”. This has been observed in [38], at least when the communication radius is infinite.

The protocol complex functor $F_R$ corresponding to this case is constructed as follows. We consider decision values to be $V = \mathbb{R}^p$, that will contain robots' individual positions. Then $F_R$ is going to be the Yoneda extension of the functor, that we still write $F_R$, which to any $(A, D) \in \Psi$ associates the chromatic simplicial set with decisions, with the set of $(B, E)$-simplexes defined as follows:

* $\emptyset$ if $B \not\subseteq A$ or if $E(b_i) \notin N_i(x_i)$ for some $i = 1, \dots, n$.

* Or when $B = \{b_0, \dots, b_m\} \subseteq A$ and $E(b_i) \in N_i(x_i)$ for all $i = 1, \dots, n$:

$$ \left\{ \left( (b_0, W_0, E(b_0)), \dots, (b_m, W_m, E(b_m)) \right) / \left\{ \begin{array}{l} W_i \subseteq A \\ \forall i, \ 0 \le i \le m, \ b_i \in W_i \\ \forall i, j, \ 0 \le i, j \le m, \ (W_i \subseteq W_j) \text{ or } (W_j \subseteq W_i) \\ \forall i, j, \ 0 \le i, j \le m, \ b_i \in W_j \Rightarrow W_i \subseteq W_j \\ \forall i, j, \ d(E(b_i), E(b_j)) \le r \end{array} \right\} \right. $$

The first condition imposes that, among the states in the next step of execution from a $(A, D)$-simplex, there can only be $(B, E)$-simplexes whose set of participating robots $B$ is a subset of the participating robots before that step of execution, i.e. $A$. Furthermore, it requires that the positions of robots $R_i$ after that step, i.e., after one move operation, are within the allowed positions from $x_i$, i.e., within $N_i(x_i)$.

In the case that those two conditions are respected, the next step is composed of $(B, E)$ simplexes with all possible views that they may get from the concurrent execution of the look-compute-move steps, corresponding exactly to the immediate snapshot conditions of Example 4.2, except those that are forbidden because of the visibility constraints between each pair of participating robots in that state: $d(E(b_i), E(b_j)) \le r$.

Similarly to Lemma 6.3, $F_R$ preserves monomorphisms, and as a left adjoint ($F_R$ is defined as a Yoneda extension in a presheaf category), it preserves colimits as well. Also, similarly to Proposition 5.1, we have a natural algebra $F_R(X) \to X$ for all $X \in \Psi^{\text{op}}\text{Set}$, which has as underlying algebra in $\Gamma^{\text{op}}\text{Set}$ functor $G$ of Example 4.2.

**Example 8.3. (Dynamic networks)**

The chromatic simplicial sets with decisions provide a simple way to extend our interpretation of patterns of communication to general dynamic network graphs. For this, we use as “decision values”

<footnote n="2">²Other difficulties are introduced, such as a visibility function depending on local states and positions that do not immediately update to the computed ones, as is often the case with physical systems. We will not consider those cases now.</footnote>
the round number, an integral number (or even a history of communication in the general case). For
any dynamic network graph G, giving a particular pattern of communication for each round $i \in \mathbb{N}$, we
produce $F_G : \Psi \to \Gamma^{\text{opSet}}$ as follows. For each $(A, D)$-simplex, with $D(a) = i$ for all $a \in A$, the
common round number, we produce the chromatic simplicial set which is $F(A)$ for the $i$th pattern of
communication in G, decorated with decision values, common to all agents, equal to $i + 1$.

**8.2. Relations between the models and interpreted protocols**

We first note that there is an obvious forgetful functor $\nu : \Psi \to \Gamma$. From this forgetful functor, we can
produce pairs of adjoint functors between $\Psi^{\text{op}}\text{Set}$ and $\Gamma^{\text{op}}\text{Set}$ as follows:

**Definition 8.4.** Consider the following functor: $c_\nu : \Psi \to \Gamma^{\text{opSet}}$ defined:

• on objects by $c_\nu(A, D) = \Gamma[A]$)

• on morphisms $f : (A, D) \to (B, E)$), we associate the morphism from $\Gamma[A]$ to $\Gamma[B]$ induced
by the inclusion map $A \subseteq B$.

We still call $c_\nu$ their left Yoneda extensions (as in Lemma 4.1), from $\Psi^{\text{op}}\text{Set}$ to $\Gamma^{\text{op}}\text{Set}$.

By Lemma 4.1, $c_\nu$ has a right adjoint we denote by $d_\nu$ from $\Gamma^{\text{op}}\text{Set}$ to $\Psi^{\text{op}}\text{Set}$.

A state-independent protocol is given by $F : \Psi^{\text{opSet}} \to \Psi^{\text{opSet}}$ that “comes” from a functor
$\Gamma \to \Psi^{\text{opSet}}$, by composition with $d_\nu$.

**Example 8.5. (Distributed robotics with unbounded visibility)**

In the case of the multirobot system of Example 8.2, where we allow for unbounded visibility, it has
been observed that task solvability reduces to standard task solvability for immediate snapshot models
[38]. Indeed, this is a consequence of the fact that in that case, the protocol complex model of Example
8.2 is exactly the same as the one for the immediate snapshot model of Example 4.2, or more precisely,
that $c_\nu$ of the former one is isomorphic to the latter one.

Let us now discuss particular state-dependent protocols which encode, for instance, the concrete
look-compute-move protocols in distributed robotics (see Example 8.7):

**Definition 8.6. (Concrete protocol)**

A concrete protocol is given by a functor $F : \Gamma^{\text{opSet}} \to \Gamma^{\text{opSet}}$ and local decision maps $f_a : \wp(\mathbb{N}) \times \mathcal{V}^\mathbb{N} \to \mathcal{V}$ which associates to each agent $a \in \mathbb{N}$ and each of the current values (for agents, including $a$), i.e. each set of participating agent $A \subseteq \mathbb{N}$ and a “local” value $v \in \mathcal{V}$, a “local” decision value for agent $a$, $f_a(A, v)$.

Supposing that $F$ is agent preserving, that is, we can only have $B$ simplexes of $F(A)$ for $B \subseteq A$,
then, we create a functor $F_f : \Psi^{\text{opSet}} \to \Psi^{\text{opSet}}$ from $F$ and $f$, as follows. It is defined by left
Yoneda extension:

• to $(B, E) \in \Psi$ we associate $F(\Gamma[B])$ that we “ decorate ” as follows so that it becomes an
element of $\Psi^{\text{opSet}}$. Each $A$ simplex of $F(\Gamma[B])$ is decorated to become an $(A, D)$ simplex as
follows. We let $D(a) = f_a(A, E)$ for all $a \in A$. This is correctly defined since $F$ is agent
preserving
• to a morphism $g : (B, E) \to (B', E')$ we associate $F(g)$ ($g$ being seen as a morphism of $\Gamma$, from $B$ to $B'$) which is defining a morphism of $\Psi^{\text{op}}\text{Set}$.

Note that any algebra $g : F(I) \to I$ lifts to give an algebra $g : F_f(I_d) \to I_d$ for any $I_d$ chromatic semi-simplicial set with decision values such that $c_\nu(I_d) = I$.

**Example 8.7. (Averaging protocol)**

We are now defining “the asynchronous average consensus concrete protocol functor” as a concrete protocol. Consider $G$, the immediate snapshot protocol complex of Example 4.2, that we consider as a functor from $\Gamma^{\text{op}}\text{Set}$ to $\Gamma^{\text{op}}\text{Set}$. Consider now $\mathcal{V}$ to be $\mathbb{R}$, the real numbers, as local values for agents, and $f_a : \wp(\mathbb{N}) \times \mathcal{V}^\mathbb{N} \to \mathcal{V}$ for all $a \in \mathbb{N}$ agent, to be

$$f_a(V, X) = X(a) + \alpha \sum_{b \in V} (X(b) - X(a)),$$

for some $0 < \alpha < 1$. The asynchronous average consensus concrete protocol functor $F_A$ is the concrete protocol given by functor $G$ and these decisions maps $f_a$, according to Definition 8.6.

**8.3. Semantics in free algebras over chromatic simplicial sets with decisions**

Recall the semantics in free algebras over csets from Section 7.3. There are similar extensions of chromatic simplicial sets with decision values to simplicial models with decision values. We write $cset_{\text{At}}^d$ for the category of simplicial models with decision values.

In this paragraph, we suppose that $F$ is a functor from $\Psi^{\text{op}}\text{Set}$ to $\Psi^{\text{op}}\text{Set}$ obtained by Yoneda extension, and that we are given a $F$-algebra over some element $I \in cset_{\text{AP}}^d$. This is typically the case given a concrete protocol as in Definition 8.6.

We extend the logics we will interpret with new predicates $q$ on a set $A_q$ of predicates on tuples of elements of $\mathcal{V}$, designed for giving properties of decision values of each agent at any step of a protocol. We interpret the extra bit in the logics as follows, denoting by $d_a$, $a \in \mathbb{N}$ the local decision value of agent $a$ in some world (that the context makes clear):

$$(Q) \quad I^\infty, x \models q((d_a)_{a \in A}) \quad \text{iff} \quad x \text{ is an } (A, D)\text{-simplex and } q((D(a))_{a \in A}) \text{ holds}$$

This extension of simplicial models to simplicial models for decisions is extremely powerful. Indeed, given a task specification as in Section 7.5 and supposing that the number of simplexes in the input and in the output complexes is finite, we can encode each one of these by an integer, and any input-output specification $T$ as a predicate $q$ on values $V = \mathbb{N}$, enumerating the valid input-output pairs of worlds. Given that classical task specification uses any iterated protocol complex $P$, this amounts to using Equation (Diam) of the semantics of our temporal-epistemic logic of Section 8.3. Task specification is then equivalent to $\Diamond q$.

**8.4. Example: task specification of robot exploration**

We now show that the language of temporal epistemic logic introduced in Section 7.1 can be used to specify tasks in distributed robotic systems, as also shown in [39], and that the free algebras model executions of the multi-robot system behavior captured in a protocol complex functor of chromatic simplicial sets with decisions from Section 8.1.
**Example 8.8. (Exploration task)**

Exploration is defined by a group of robots $R_i$ at positions $x_i$ capable of movement (updating their positions) and observing their environment. They execute look-compute-move cycles and their possible movement updates are defined by the robot's dynamics<fnref n="3" /> and encoded in their accessible states $N_i(x_i)$, while the possible observations are constrained by an observation range $r$. Formally, their environment $E$ is the topological subspace of $\mathbb{R}^d$ obtained from a basis of open balls using the robot's observation range.

Each robot decides a new position to take and how much of the space has been explored. This information is expressed as atomic propositions $\exp_U \in \mathbf{Aq}$ associated to each possible observation $U \in \mathit{Open}(E)$. Those propositions alongside the temporal epistemic logic of Section 7.1 form the exploration language $\mathcal{L}_{\mathit{exp}}$ needed to describe the robot task of exploration.

$$ \varphi ::= \exp(U) | \neg\varphi | (\varphi \land \varphi) | K_r\varphi | D_B\varphi | \diamond\varphi $$

where $\exp(U) \in \mathbf{Aq}$, $\mathbf{r} \in A$ and $B \subseteq A$.

A multi-robot system execution, modeled with an object $I^\infty$ of the free $F_R$-algebra over some “set” of initial states $I \in \mathit{cset}_{\mathbf{Aq}}$, is said to be consistent with exploration[39] if it satisfies:

* Exploration agency: an explored region has been explored by at least one robot.

$$ I^\infty \models \exp(U) \rightarrow D_{\Pi} \exp(U) \qquad (4) $$

* Exploration independence: distributed exploration knowledge comes from the union of the respective robot's explored regions.

$$ I^\infty \models D_B \exp(U) \rightarrow \bigwedge_{\mathbf{r} \in B} K_r \exp(V_r) \text{ such that } \bigcup_{\mathbf{r} \in B} V_r = U \qquad (5) $$

* Stable exploration statements: an explored region remains explored forever. For any region $U$

$$ I^\infty \models \bigwedge_{\exp(U) \in \mathcal{L}_{\mathit{exp}}} \exp(U) \rightarrow \Box \exp(U) \qquad (6) $$

* Stable exploration knowledge: the knowledge of an explored region remains known forever. For any $\mathbf{r} \in \Pi$, and any region $U$

$$ I^\infty \models K_r \exp(U) \rightarrow \Box K_r \exp(U) \qquad (7) $$

It becomes evident that exploration of a space $X$ is satisfied whenever $I^\infty \models \diamond D_A \exp(X)$, when a robot terminates as soon as it knows that the entire space has been explored. Alternatively, one can require that robots only terminate whenever it is common knowledge that the mission has finished, i.e., $I^\infty \models \diamond \bigwedge_{\mathbf{r} \in A} K_r X$.

<footnote n="3">³The dynamics of a robot is defined using a system of ODEs that can be arbitrarily complex. As this is not the focus of this paper, we will consider only a point-mass system, i.e., a point in space capable of moving freely in any direction.</footnote>
9. Conclusion

In this paper, we showed that the round-based protocol complex approach of [1] falls nicely into the categorical framework of algebras over chromatic augmented pre-simplicial sets (csets). The protocol complexes themselves are naturally defined as functors from csets to csets, that are Yoneda extensions of very simple functors. This algebraic formulation naturally leads to a temporal-epistemic logics, that is useful for specification, and verification purposes.

Finally, we paved the way for future extensions, leading to wider application areas such as dis-
tributed robotics, where a notion of local state has to be taken into account for even defining the
corresponding protocol complexes.

As a note in Appendix A (this is not the main subject of this paper), this formulation allows simple reasoning for finding topological invariants of the protocol complex. This is indeed linked to some of the logical properties that we develop in this paper, as developed in e.g. [14], but this is left for future work.

References

[1] Herlihy M, Feichtner-Kozlov D, Rajsbaum S. Distributed Computing Through Combinatorial Topology. Morgan Kaufmann, Amsterdam, 2014. ISBN 978-0-12-404578-1.

[2] Goubault É, Ledent J, Rajsbaum S. A Simplicial Complex Model for Dynamic Epistemic Logic to study Distributed Task Computability. *Information and Computation*, 2021. **278**:104597. doi:10.1016/j.ic.2020.104597.

[3] Manna Z, Pnueli A. Temporal verification of reactive systems: safety. Springer-Verlag, Berlin, Heidelberg, 1995. ISBN 0387944591.

[4] Herlihy MP, Wing JM. Linearizability: a correctness condition for concurrent objects. *ACM Trans. Program. Lang. Syst.*, 1990. **12**(3):463–492. doi:10.1145/78969.78972. URL https://doi.org/10.1145/78969.78972.

[5] Moran S, Wolfstahl Y. Extended impossibility results for asynchronous complete networks. *Information Processing Letters*, 1987. **26**(3):145–151. doi:https://doi.org/10.1016/0020-0190(87)90052-4. URL https://www.sciencedirect.com/science/article/pii/0020019087900524.

[6] Biran O, Moran S, Zaks S. A Combinatorial Characterization of the Distributed 1-Solvable Tasks. *J. Algorithms*, 1990. **11**(3):420–440. doi:10.1016/0196-6774(90)90020-F. URL https://doi.org/10.1016/0196-6774(90)90020-F.

[7] Castañeda A, Rajsbaum S, Raynal M. Unifying Concurrent Objects and Distributed Tasks: Interval-Linearizability. *J. ACM*, 2018. **65**(6):45:1–45:42. doi:10.1145/3266457.

[8] Goubault É, Ledent J, Mimram S. Concurrent Specifications Beyond Linearizability. In: 22nd International Conference on Principles of Distributed Systems, OPODIS 2018, December 17-19, 2018, Hong Kong, China. 2018 pp. 28:1–28:16. doi:10.4230/LIPICS.OPODIS.2018.28.

[9] R Fagin YM J Halpern, Vardi M. Reasoning About Knowledge. MIT Press, 1995.

[10] Knight S. The Epistemic View of Concurrency Theory. (Le point de vue epistémique de théorie de la concurrence). Ph.D. thesis, École Polytechnique, Palaiseau, France, 2013.
[11] Goubault É, Ledent J, Rajsbaum S. A simplicial complex model for dynamic epistemic logic to study distributed task computability. *Inf. Comput.*, 2021. **278**:104597. doi:10.1016/J.IC.2020.104597. URL https://doi.org/10.1016/j.ic.2020.104597.

[12] Goubault E, Kniazev R, Ledent J, Rajsbaum S. Simplicial models for the epistemic logic of faulty agents. *Bol. Soc. Mat. Mex.*, 2024. **30**(90). URL https://doi.org/10.1007/s40590-024-00656-x.

[13] Goubault É, Kniazev R, Ledent J, Rajsbaum S. Semi-Simplicial Set Models for Distributed Knowledge. In: LICS. 2023 pp. 1–13. doi:10.1109/LICS56636.2023.10175737. URL https://doi.org/10.1109/LICS56636.2023.10175737.

[14] Goubault É, Ledent J, Rajsbaum S. A Simplicial Complex Model for Dynamic Epistemic Logic to study Distributed Task Computability. In: Orlandini A, Zimmermann M (eds.), Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018, volume 277 of *EPTCS*. 2018 pp. 73–87. doi:10.4204/EPTCS.277.6.

[15] Winkler K, Schmid U. An Overview of Recent Results for Consensus in Directed Dynamic Networks. *Bull. EATCS*, 2019. **128**. URL http://bulletin.eatcs.org/index.php/beatcs/article/view/581/585.

[16] MacLane S. Categories for the Working Mathematician. Springer-Verlag, New York, 1971. Graduate Texts in Mathematics, Vol. 5.

[17] Adámek J, Porst H. On Varieties and Covarieties in a Category. *Math. Struct. Comput. Sci.*, 2003. **13**(2):201–232.

[18] Trnková V, Adámek J, Koubek V, Reiterman J. Free algebras, input processes and free monads. *Commentationes Mathematicae Universitatis Carolinae*, 1975. **16**(2):339–351.

[19] Moses Y, Rajsbaum S. A Layered Analysis of Consensus. *SIAM J. Comput.*, 2002. **31**(4):989–1021.

[20] Baltag A, Renne B. Dynamic Epistemic Logic. In: The Stanford Encyclopedia of Philosophy, see https://plato.stanford.edu/archives/win2016/entries/dynamic-epistemic/. Metaphysics Research Lab, Stanford University, 2016.

[21] Ditmarsch Hv, van der Hoek W, Kooi B. Dynamic Epistemic Logic. Springer, 2007. doi:10.1007/978-1-4020-5839-4.

[22] Baltag A, Moss L, Solecki S. The logic of common knowledge, public announcements, and private suspicions. In: TARK VII. 1998 pp. 43–56. doi:10.1007/978-3-319-20451-2_38.

[23] Eilenberg S, Zilber JA. Semi-simplicial complexes and singular homology. *Annals of Mathematics*, 1950. pp. 499–513.

[24] Riehl E. A Leisurely Introduction to Simplicial Sets.

[25] Mac Lane S, Moerdijk I. Sheaves in Geometry and Logic a First Introduction to Topos Theory. Springer New York, 1992. ISBN 9781461209270 1461209277.

[26] Gabriel P, Zisman M. Calculus of fractions and homotopy theory. Springer-Verlag Berlin, New York, 1967.

[27] Borowsky E, Gafni E. Immediate Atomic Snapshots and Fast Renaming (Extended Abstract). In: Anderson J, Toueg S (eds.), Proceedings of the Twelfth Annual ACM Symposium on Principles of Distributed Computing, Ithaca, New York, USA, August 15-18, 1993. ACM, 1993 pp. 41–51. doi: 10.1145/164051.164056. URL https://doi.org/10.1145/164051.164056.
[28] Goubault É, Mimram S, Tasson C. Geometric and combinatorial views on asynchronous computability. *Distributed Comput.*, 2018. **31**(4):289-316.

[29] Kozlov DN. Chromatic subdivision of a simplicial complex. *Homology, Homotopy and Applications*, 2012. **14**(2):197–209.

[30] Kuhn F, Oshman R. Dynamic Networks: Models and Algorithms. *SIGACT News*, 2011. **42**(1):82-96.
doi:10.1145/1959045.1959064. URL https://doi.org/10.1145/1959045.1959064.

[31] Castañeda A, van Ditmarsch H, Rosenblueth DA, Velázquez DA. Pattern Models: A Dynamic Epistemic Logic For Distributed Systems. *The Computer Journal*, 2024. **67**(7):2421-2440. doi:10.1093/comjnl/bxa016. URL https://doi.org/10.1093/comjnl/bxa016.

[32] Coulouma É, Godard E, Peters JG. A characterization of oblivious message adversaries for which Consensus is solvable. *Theor. Comput. Sci.*, 2015. **584**:80-90. doi:10.1016/j.tcs.2015.01.024. URL https://doi.org/10.1016/j.tcs.2015.01.024.

[33] Kurz A. Logics for Coalgebras and Applications to Computer Science. BoD - Books on Demand, 2001.
ISBN 9783831112494.

[34] Mac Lane S, Moerdijk I. Sheaves in Geometry and Logic a First Introduction to Topos Theory, 1992.
URL http://link.springer.com/book/10.1007/978-1-4612-0927-0.

[35] Karazeris P, Protsonis G. Left Kan Extensions Preserving Finite Products. URL http://old.math.upatras.gr/~pkarazer/publications/topsift.pdf.

[36] Goubault É, Ledent J, Rajsbaum S. A Simplicial Model for KB4_n: Epistemic Logic with Agents That May Die. In: 39th International Symposium on Theoretical Aspects of Computer Science, STACS 2022. 2022 p. 33:1-33:20. doi:10.4230/LIPIcs.STACS.2022.33.

[37] Goubault E, Kniazev R, Ledent J, Rajsbaum S. Simplicial Models for the Epistemic Logic of Faulty Agents. *CoRR*, 2023. abs/2311.01351. doi:10.48550/ARXIV.2311.01351. URL https://doi.org/10.48550/arXiv.2311.01351.

[38] Alcántara M, Castañeda A, Flores-Peñaloza D, Rajsbaum S. The topology of look-compute-move robot wait-free algorithms with hard termination. *Distrib. Comput.*, 2019. **32**(3):235-255. doi: 10.1007/s00446-018-0345-3. URL https://doi.org/10.1007/s00446-018-0345-3.

[39] Cignarale G, Felber S, Goubault E, Hummes Flores B, Rincon Galeana H. Knowledge in Multi-Robot Systems: An Interplay of Dynamics, Computation and Communication. doi:10.48550/arXiv.2501.18309. 2501.18309.

[40] Björner A. Nerves, fibers and homotopy groups. *Journal of Combinatorial Theory, Series A*, 2003. **102**(1):88-93. doi:https://doi.org/10.1016/S0097-3165(03)00015-3. URL https://www.sciencedirect.com/science/article/pii/S0097316503000153.

[41] Éric Goubault, Mimram S, Tasson C. Iterated Chromatic Subdivisions are Collapsible. *Applied Categorical Structures*, 2014. p. 1–42. doi:10.1007/s10485-014-9383-6. URL http://dx.doi.org/10.1007/s10485-014-9383-6.
**A. Topological invariants of the protocol complex**

The formulation of the protocol complex as a certain left Yoneda extension allows, in some situations,
to get the homology type of the protocol complex, for free. As well-known, this is instrumental for
showing impossibility of some fault-tolerant decision tasks, such as consensus, in e.g. asynchronous
distributed systems.

First, we remind the reader of the generalized nerve theorem of [40]. But before that, we need a
few definitions:

**Definition A.1.** Let $(X_i)_{i \in I}$ be a family of sets. The nerve of this family of sets is the simplicial complex $\mathcal{N}(X_i)$ which has:

• as vertices, the indexes $i \in I$,

• as simplexes $\sigma$, subsets of $I$ such that $\bigcap_{i \in \sigma} X_i \neq \emptyset$.

Said differently, the nerve $\mathcal{N}(X_i)$ is the nerve (in the category theory sense, or in the classical poset meaning) of the diagram $D^X$ given by the canonical inclusion maps of all non-empty intersections $X_{i_1} \cap \dots \cap X_{i_t}$ into all its sub-intersections.

**Theorem A.2. ([40])**

Let $\Delta$ be a connected regular CW complex and $(\Delta_i)_{i \in I}$ a family of subcomplexes such that $\Delta = \bigcup_{i \in I} \Delta_i$ (i.e. a cover of $\Delta$). Suppose that every non-empty finite intersection $\Delta_{i_1} \cap \Delta_{i_2} \cap \dots \cap \Delta_{i_t}$ is $(k-t+1)$-connected, $t \ge 1$. Then there is a map $f$ from the $\Delta$ to the geometric realization of the nerve $\mathcal{N}(\Delta_i)$ inducing isomorphisms of homotopy groups $f_j^* : \pi_j(\Delta) \sim \pi_j(\mathcal{N}(\Delta_j))$ for all $j \le k$.

**Example A.3. (Immediate snapshot example)**

By [41], the image of any simplex by $G!$ is collapsible, hence contractible. A direct application of
Theorem A.2 shows that $G!(I)$ has the same homotopy type as $I$, for any input simplicial complex $I$.

Indeed, for any input complex $I$, $I$ is covered by the subcomplexes $\Delta_{\sigma}^I$ generated by all maximal
simplexes $\sigma$ of $I$. All these complexes are contractible, with non-empty intersections being a subcom-
plex generated by a unique simplex, hence being contractible as well. This is due to the fact that $I$ is
a simplicial complex, it would not be true in general if $I$ was a simplicial set (the intersection of two
closed simplexes may be disconnected, for instance). Furthermore, $I$ is the colimit of the $\Delta_{\sigma}^I$ over the
diagram $D^I$ given by the canonical inclusion maps of all non-empty intersections $\Delta_{\sigma_{i_1}}^I \cap \dots \cap \Delta_{\sigma_{i_t}}^I$,
identified with the subcomplex $\Delta_{i_1, \dots, i_t}^I$ generated by a unique simplex, into all its sub-intersections
$\Delta_{i_1, \dots, \hat{i}_k, \dots, i_t}^I$. By Theorem A.2 applied to a large enough $k$ (at least the maximal dimension of sim-
plexes in $I$), $\pi_j(I)$ is isomorphic to $\pi_j(\mathcal{N}(\Delta_i^I))$, i.e. $I$ has the same homotopy type as $\mathcal{N}(\Delta_i^I)$.

As $G!$ commutes with colimits, Lemma 6.3, $G!(I)$ is the colimit over $G!(\Delta_{\sigma}^I)$. $\sigma$ being a maximal
simplex, this is the representable functor in $\Gamma^{\text{op}}\text{Set}$ $\Gamma(., A_{\sigma})$, where $A_{\sigma}$ is an object of $\Gamma$ (a set of
colors). By definition of a left Yoneda extension, $G!(\Delta_{\sigma}^I)$ is thus equal to the cset $G(A_{\sigma})$. Furthermore,
$G!(D^I)$ is the diagram of inclusions $G!(\Delta_{i_1, \dots, i_t}^I)$ into $G!(\Delta_{i_1, \dots, \hat{i}_k, \dots, i_t}^I)$, by Lemma 6.3 again, which
again, as these complexes $\Delta_{i_1, \dots, i_t}^I$ are generated by a unique simplex $\Gamma(., A_{i_1, \dots, i_t})$, is the diagram of inclusions $G(A_{i_1, \dots, i_t})$ into $G(A_{i_1, \dots, \hat{i_k}, \dots, i_t})$. This means that the $G(A_\sigma)$ where $\sigma$ ranges over the maximal simplexes of $I$ form a cover of $G!(I)$, and has the same underlying diagram of inclusions as $D^I$. By Theorem A.2, as $G(A_\sigma)$ and all its non-empty intersections $G(A_{i_1, \dots, i_t})$ are contractible, $G!(I)$ has the same homotopy type again as $\mathcal{N}(D^I)$ i.e. as $I$.

**Example A.4. (Synchronous broadcast example)**

Unfortunately, even the generalized nerve theorem of [40] does not help with the synchronous broadcast case. In this case, we need to use the Mayer-Vietoris exact sequence:

<figure><img src="image_16.png" /></figure>

This allows for instance, for an inductive computation of the homology groups of $F_!(X)$ where $X$ is a binary sphere of dimension $n \ge 2$. In that case, we decompose $X$ as $X_1 \cup X_2$ where $X_1$ is the north hemisphere of $X$, $X_2$ is the south hemisphere of $X$ and $X_1 \cap X_2$ is the binary sphere of dimension $n-1$. As $F_!$ preserves colimits, Lemma 6.3, we get:

<figure><img src="image_17.png" /></figure>

where the diagram is uniformly 0 from dimension $n+1$ on. This allows in particular to get simple inequalities on the rank of the various $H_i[F_!(X)]$.