Epistemic and Topological Reasoning
in Distributed Systems

The combinatorial topology approach to distributed computing has been shown to be powerful for studying solvability of fundamental distributed problems such a consensus, set agreement and renaming [42]. However, the current approach has a clear limitation as it can be applied only to distributed problems that can be modeled as (distributed) tasks. A task models a one-shot distributed problem where each process starts with a private input, and the processes are required to communicate with each other in order to decide private outputs that satisfy the task’s specification. Nonetheless, there are fundamental distributed problems that cannot be specified as tasks [17, 18]. An important class of such problems are concurrent objects (or data structures), e.g., queues, stacks, trees and dictionaries. One seeks for implementations of them that are linearizable [43]. Roughly speaking, in a concurrent object, a process can perform an unbounded number of the operations provided by the object (differently from tasks where there is a single operation) and, in a linearizable implementation, responses to operations must be valid for the object that is implemented, somehow respecting the order operations are performed in a given execution.

Formally, a task is a triple $T=⟨I,O,\mathrm{\Delta }⟩$, where $I$ and $O$ are input and output complexes specifying the input and output domains of the task, and $\mathrm{\Delta }$ is a carrier map specifying the complex $\mathrm{\Delta }(\sigma )\subseteq O$ with valid outputs for each input simplex $\sigma \in I$. An execution $E$ is valid for the task if $\tau \in \mathrm{\Delta }(\sigma )$, where $\sigma$ and $\tau$ are the simplexes with inputs and outputs in $E$, respectively.

Our discussion centered around finding a topological specification for concurrent objects. It first centered on previous work [17, 18], which already showed that tasks are too weak to even represent a one-shot queue, where each process can only access once by performing a fixed operation. The main problem is that carrier maps of tasks have limited ability to specify the order in which operations are performed in an execution.

The aforementioned work defined refined tasks (called long-lived task in [17]), where a vertex in the input complex represents a specific invocation to the object by a specific process. When using a simplex to represent an input configuration, multiple invocations of the same operation by the same process are represented by multiple distinct vertices in the simplex. Starting from any simplex in the input complex, each execution $E$ specifies a simplex ${\tau }_E$ where each vertex of ${\tau }_E$ consists of a process identifier, an invocation to the object by this process, the response to this invocation in $E$, and the set-view when the response was returned. A set-view is the set of all invocations (by all processes) on the object up to a particular point in the execution. The set of set-views in ${\tau }_E$ fully captures the interleaving of operations in the execution $E$. The output complex consists of simplexes ${\tau }_E$ specified by all possible executions (concurrent and sequential) $E$ whose operations appear in simplexes of the input complex. A refined task is a triple $T=⟨I,O,\mathrm{\Delta }⟩$ where $\mathrm{\Delta }(\sigma )\subseteq O$ contains simplexes ${\tau }_E$ specified by all possible sequential $E$ where processes perform the operations in a simplex $\sigma \in I$, in some order. A concurrent execution $E^{\prime }$ with operations in a simplex $\sigma \in I$ is considered valid for the refined task if there exists a simplex ${\tau }_E\in \mathrm{\Delta }(\sigma )$ such that (1) the outputs to operations in $E^{\prime }$ and $E$ agree, and (2) the set-view of each vertex in ${\tau }_{E^{\prime }}$ contains the set-view of its corresponding vertex in ${\tau }_E$.

Refined tasks have been shown to be expressive enough to model any linearizable concurrent object. However, this does not seem to resolve the limitation mentioned above because the notion of solvability for refined tasks is based on two components: outputs and set-views. The problem is that set-views are features of the execution, i.e., they are not produced or implied by processes’ states. It is not clear how set-views can be captured by simplicial maps in a way that the combinatorial topology approach can be applied to study solvability of refined tasks. Let us recall that in the combinatorial topology approach protocols are modeled as simplicial maps that specify outputs as function on only process states, and the main question that needs to be answered is whether there exists a simplicial map from the protocol complex to the output complex, respecting the specification of the task in question. It may be possible that refined tasks can be used to study solvability of linearizable concurrent object $S$ in an indirect manner as suggested in [33], where a task $T$ is constructed such that if there is a linearizable implementation of $S$ then $T$ is solvable.

The group discussed two possible alternative approaches to specify concurrent objects that may be more suitable for the combinatorial topology approach. Applications of these approaches remain to be seen.

While both DEL and IS provide means to track the manner in which knowledge and belief change over time in a multi-agent system, the two approaches differ dramatically in the way that they model the effect that actions have. In DEL, actions operate directly on the epistemic state of the system (this epistemic state is represented by a Kripke structure). For every action, the framework must provide an action model, which maps a Kripke structure and an action to a new Kripke structure, thereby describing the manner in which the epistemic state changes when the action is performed. In IS actions are taken to modify the physical configuration (or global state) of the system. As in automata theory, this is modeled by way of a transition function, mapping a configuration and an action to the configuration that results from performing the action. The epistemic state of the system in IS is also modeled using a Kripke structure, but this structure is induced by the system configurations, where each agent’s indistinguishability relation is determined by its local state.

In the IS way of modeling of distributed systems, based on the runs-and-systems framework [31], agent protocols and the environment are outside of the formal logic used for epistemic reasoning. In fact, they are represented using transition systems (TS) which are the primary objects of study. Since the executions of a distributed protocol can typically be described in terms of a transition system (see [47]), the IS approach can readily be applied to a broad range of distributed systems problems.

In DEL [26], agent protocols (as well as the environment) can be expressed in the formal logic used for epistemic reasoning. In particular, action models enable one to model many forms of communication between the agents while focusing on capturing the resulting knowledge evolution of the involved agents. Moreover, precondition formulas can be used to tie communication actions to particular epistemic states of the agents (that are necessary to hold when communicating). Works such as [37], which even connect DEL and combinatorial topology, show that the idea of using DEL to help with topological reasoning about distributed systems is promising.

DEL and IS have been used for the analysis of communication protocols. Specific features of the protocols themselves indicate which framework fits best. The features we are looking at are a) temporal aspects (synchronous versus asynchronous communications) and b) the private versus public nature of the information contained in the events or actions that happen as part of the protocol. Here, we note that in DEL, time is not explicitly represented. Embeddings from DEL into IS (or rather into temporal epistemic logics) have been proposed. This includes both synchronous embeddings [10], wherein the execution of an action corresponds to a clock tick, and asynchronous embeddings [21], wherein histories of actions of variable length correspond to time in some way. While some believe that DEL and IS can be extended with ingredients so they can model the same kind of protocols, the starting base of these frameworks does differ. The built-in features of the starting base (such as the temporal aspects in IS and the action models in DEL) will make the application of one or the other framework a more straightforward choice for a given type of protocol. For instance when we focus on cryptographic protocols with complex cryptographic primitives as part of the actions or events that happen in the protocol, we see an added advantage of starting with DEL which offers us the expressive power of modeling the security aspects in the actions separately and allows us to automatically compute the state-transitions via its product update mechanism. DEL is used in the study of cryptographic protocols in works like [44, 20, 23, 30].

An advantageous feature of DEL is the fact that its built-in model update mechanism makes it immediately well-suited for automated model checking tasks. The implementation was done in different programming languages, but the most elaborate tool uses Haskell in DEMO [29]. The power of DEMO for model checking tasks has been illustrated on a small number of well-known sample protocols including comparison to temporal epistemic model checkers like MCK [27], which is based on IS modeling.

A disadvantage of DEL in general is the potential blowup of the model (or the precondition formulas). There are various reasons for such a blowup. As the models used in DEL are small (updates, and their temporal interpretation, are computable from an initial model and the sequence of actions), complexities with respect to model size are high [3]. Another reason is the iteration of action models, which leads to exponential growth of the size with each model update. This can be addressed with symmetry reductions [34], restriction to point-generated submodels [12], dedicated tools for specific frame classes (such as models with equivalence relations) instead of arbitrary binary relations [29], and bisimulation contraction [12].

A feature of DEL often forgotten is that such logics and frameworks are essentially logics of observation, not of action. One can investigate the consequence of actions if they were to happen, but one cannot state “let this action happen now”. This is of course very different from IS. Once we add factual change to the DEL framework, this drawback is somewhat overcome. Now there are actions such as turning on and off the light, setting values of keys, etcetera. But agency remains lacking.

Operationalizing the implicit Kripke model construction resulting from executing the system primarily requires the construction of action models for typical communication protocols considered in epistemic analysis via IS. The challenge here is to develop action models that avoid state explosion. One promising starting point could be communication patterns, updates that compare in interesting ways to action models [55, 15, 14]. The availability of such action models would open up some interesting avenues such as:

• $\mathrm{■}$

  Could correctness proofs of protocols formulated via suitable precondition formulas of such action models be automated, via analyzing the Kripke model obtained by the product updates w.r.t. satisfying the desired properties? This would replace the translation of knowledge-based protocols obtained via IS to TS, and the obligatory proof that the resulting protocol guarantees that the agents attain their respective necessary level of knowledge.

  Good target practice will be to model the consensus protocol for processes with send-omission faults from [1] in DEL, by (i) defining an action model for send-omission faults, (ii) modeling the protocol implementations via suitable precondition formulas, and (iii) generating and analyzing the Kripke model after suitably many rounds. We were optimistically thinking of including these results already in the report, however that was a bridge too far. Still, we are committed to this and other benchmarks to compare DEL and IS.

• $\mathrm{■}$

  An area in DEL that is highly targeted towards protocols and automation is that of epistemic planning [13, 6, 48], and in particular concerning decidability of epistemic planning problems [2, 46]. Could epistemic planning techniques be used for synthesizing protocols in a distributed setting?

The IS approach has been used to provide insights into the interaction between knowledge and communication in distributed systems ([39, 19, 7]), has allowed to generalize existing protocols ([40]), and to design optimal and state-of-the-art protocols solving well-known problems ([28, 50, 35, 16, 1]). These works provide insight into the role of synchrony and partial synchrony, refine our analysis of achievable types of optimality in different models of distributed computation, and into various aspects of fault-tolerance. The Knowledge of Preconditions principle [49], which is naturally formulated in IS, provides model-independent theorem capturing the connection between knowledge and action in multi-agent systems. It has been shown to facilitate the design and analysis of efficient distributed systems protocols. Although protocols are not explicitly represented in the IS framework, it is possible to consider high-level “knowledge-based programs” in this setting, in which actions depend on tests for knowledge. In general, however, such programs are specifications and do not always uniquely determine the agents’ behavior. Finding ways to implement them may be challenging. The more developed literature applying IS for the study of distributed computing can serve as an example and inspiration for directions in which DEL may be expanded. Fundamentally, DEL can be viewed as a subclass of IS. Its added declarative nature described above comes at a cost, however. Modeling and studying aspects of timing, including the role of synchrony, asynchrony and partial synchrony have been carried out successfully using the IS framework, while handling asynchrony, and partial synchrony appear to pose significant challenges for DEL. Similarly, incorporating failures, which have been studied in many IS settings, seems likely to give rise to cumbersome DEL models.

In order to be able to apply the IS framework, one only needs a description of the set of possible histories of a system, and a clear definition of the local states of agents in every configuration. As mentioned above, the fact that systems are often described by way of a transition system obviates the need to translate a given system into the formalism. Treating, say, an existing internet protocol using DEL would typically require a significant reformulation effort. Making DEL more flexible in this sense seems to be a considerable albeit worthwhile challenge. Finally, while the IS framework has given rise to new and improved protocols as well as tight bounds and impossibility results in different models of distributed computing, this has not been a focus of DEL works. It will be very interesting to see how well DEL can match such tasks, in light of the results obtained using IS.

Let us now model belief ($B_a$) instead of knowledge ($K_a$). Unlike knowledge, belief may be incorrect. A common way to model belief in modal logic, interpreted on Kripke models, is by way of relations that are serial, transitive, and Euclidean, for which the logic is KD45. That is, it satisfies:

• $\mathrm{■}$

  $B_a\phi \to {\widehat{B}}_a\phi$ (consistency)

• $\mathrm{■}$

  $B_a\to B_a{B}_a\phi$ (positive introspection)

• $\mathrm{■}$

  ${\widehat{B}}_a\phi \to B_a{\widehat{B}}_a\phi$ (negative introspection)

This is known as consistent belief [25] and also as irrevocable belief (or as conviction) [54]. Recalling the KD45 “balloons” (clusters of indistinguishable worlds) with “ropes” (asymmetric pairs in the accessibility relation) from isolated worlds pointing to these clusters, a way to model belief on complexes is with a belief function $f:𝒱(C)\to 𝒱(C)$ that is an idempotent and color-preserving vertex map. It is not a chromatic map as it may not preserve other simplices. Let $X_a$ be the vertex of color $a$ that belongs to a facet $X$. Belief is now defined as

If, for a world $v$, $f(v)=v$, belief becomes knowledge. The map needs to be idempotent to ensure that the properties of belief hold, we can see the map $f$ as “pointing” vertex $v$ to a cluster of $f(v)$ adjoining facets, in words referring to a corresponding Kripke model, to a set of $b$-indistinguishable worlds.

As an example, we reconsider the model above but now enriched with a belief function that maps vertex $a0$ to vertex $a2$ and otherwise maps all vertices to themselves, as below.

This represents that in local state $a0$ agent $a$ believes that her local state is $a2$ and that the global state is $Z$. Observe that this also implies that $a$ incorrectly believes that the value of her local state is $2$ and not $0$. However, a reasonable assumption may be that an agent correctly knows its local state, and may only be mistaken about what it believes to be the local states of other agents. (This assumption underlies some of our later epistemic explorations, wherein different vertices of the same colour jointly represent an agent’s beliefs.) We now have that, for example,

and so forth … Note that we only have one modality in the logical language here, the informal “agent $a$ knows” and “agent $b$ knows” above are only written because in the facets (global states) where these formulas are interpreted the agents’ beliefs are correct.

As a side issue, let us now consider the belief function $g$ such that $g(a0)=a2$, $g(c0)=c1$, and otherwise the identity. In the model ${𝒞}^i$, the distributed knowledge of agents $a$ and $c$ in facet $W$ is represented by the edge $\{c0,a0\}$. Whereas in the model ${𝒞}^{ii}$ but with belief function $g$, agents $a$ and $c$ have distributed belief embodied in the edge $\{c1,a2\}$. Group epistemic notions other than for knowledge were not discussed, but might worth to be investigated later.

The belief function is an enrichment of the simplicial model. It does not, on first sight, seem very topological in nature, and therefore not very simplicial. It rather looks like an accessibility relation between the worlds of a Kripke model. In fact, taken as a relation, a belief function is serial, transitive, and Euclidean, just as required for belief. Let us see how we can stretch this analogy a bit further before we return to more topological interpretations, in Subsection 4.3.3.

Now assume any function that is a transitive relation. Consider the belief function $f$ that maps vertex $a0$ to $a1$ and vertex $a1$ to $a2$, and therefore, by transitivity, $a0$ to $a2$. As follows (transitivity is implicit):

This induces a (strict) total order on the $a$ vertices such that $a0>a1>a2$, with an associated weak total order $\ge$. We can now interpret this total order as sorting comparable $a$-vertices into more and less plausible, where in this case $a2$ is most plausible, $a1$ somewhat less, and $a0$ least, by analogy of the plausibility models of [4] (and not dissimilar to [8, 22], see also [11]). Let us additionally write $a0\geqq a2$ to indicate that $a2$ is the most plausible local state for $a$ in this total order (or, dually, $\le$ and $\leqq$), $\equiv$ for equally plausible, and $\sim$ for comparable.

We now can assume a multi-modal language and define notions of belief (revocable/defeasible belief), safe belief (strong belief), and knowledge. Depending on one’s preferred dialect this can be done in different ways. In the semantics for $a$-adjoining facets we would get, where $X\in ℱ(C)$:

The relation $\ge$ between $a$-vertices induces a relation ${\ge }_a$ between facets, namely such that $X{\ge }_{a}Y$ if $X_a\ge Y_a$, and analogously we can induce relations ${\geqq }_a$, ${\equiv }_a$ and ${\sim }_a$. Note that as a consequence all facets containing a given local state for agent $a$ are equally plausible for her. Using this relation between facets, for the semantics of defeasible belief $B_a$ we would now get (where those for ${\mathrm{\square }}_a$ and $K_a$ are analogous) the following equivalent semantics, where for good measure we have added two more equivalent formulations. Which one looks most simplicial?

As an example of the semantics above we can easily determine in the simplicial model ${𝒞}^{iii}$ that

This notion of knowledge is different from the standard notion of simplicial knowledge applied in model ${𝒞}^i$. We recall that ${𝒞}^i,X\vDash K_a(0_b\vee 1_b)$, as knowledge in $X$ means truth in $W$ and $X$. Whereas ${𝒞}^{iii},X\vDash ̸K_a(0_b\vee 1_b)$, as this ‘novel’ knowledge in $X$ means truth in $W,X,Y,Z$, and $0_b\vee 1_b$ is false in $Z$.

This can be adjusted by tentatively proposing a belief quotient of a simplicial model with respect to a belief function inducing a total order $\le$ as above. As we will see this may not always be a simplicial model, but it seems it always will be a simplicial set. The belief quotient of a complex $𝒞=(C,\chi ,\mathrm{\ell })$ would be ${𝒞}_{\le }=(C_{\le },{\chi }_{\le },{\mathrm{\ell }}_{\le })$ as follows. Let for any $v\in 𝒱(C)$ vertex $v_{\le }$ be defined as $\{w\in 𝒱(C)\mid w\sim v\}$, then $𝒱(C_{\le }):=\{v_{\le }\mid v\in 𝒱(C)\}$. Note that the choice of vertex determines its colour, so $v_{\le }$ is the equivalence class of all vertices $w$ that are more or less plausible then $v$ for agent $\chi (v)$, so there is no need for an ‘$a$’ as in ${\le }_a$. The faces of $C_{\le }$ now are $Y$ for which there is a $Z\in C$ with $Y=\{v_{\le }\mid v\in Z\}$. As comparable vertices may have different labelings of propositional variables, proposing ${\mathrm{\ell }}_{\le }(v_{\le }):=\bigcup \{\mathrm{\ell }(v)\mid w{\sim }_{a}v\}$ may not be very useful. However, we recall that requiring labelings to be the same for comparable vertices was already mentioned as a reasonable assumption for belief functions. Let us therefore assume that all $\le$-comparable vertices have the same labeling. We now can produce some nice examples.

In ${𝒞}^i$, the variables $0_a,1_a,2_a$ were only true in $a0,a1,a2$, respectively. Let us now, instead, assume that they are true in all three $a0,a1,a2$ so that $0_a\leftrightarrow 1_a$ and $1_a\leftrightarrow 2_a$ on the model. We now simply take $a{0}_{\le }$ to be $a0$ itself. Given that, and some visual trickery, the belief quotient of ${𝒞}^{ii}$ is ${𝒞}^{iv}$ below.

Similarly, the belief quotient of ${𝒞}^{iii}$ is ${𝒞}^v$ below, where we note that this is a simplicial set, as the edges $\{a0,b1\}$ and $\{a0,c1\}$ occur twice in the complex (denoted by the double-lined edge).

This representation does not make any difference for the semantics, but we are now back to a possible more pleasing, and familiar, notation for more and less plausible facets adjoining a vertex. In ${𝒞}^{iv}$ we have that vertex $a0$ intersects with $W,X,Z$ where $W$ and $X$ are equally plausible and $Z$ is more (and most) plausible. In ${𝒞}^v$ we have that vertex $a0$ intersects with $W,X,Y,Z$ where $W$ and $X$ are equally plausible, both are more plausible than $Y$, which is more plausible than $Z$.

A simple belief function for irrevocable belief, or a more complex belief function to model defeasible or strong belief, or even knowledge in a different way, is not a very topological tool. Nor is ordering the different facets intersecting in a vertex in the belief quotient version. It was widely discussed how to make such ideas into something more topological. Reconsidering the simplicial model ${𝒞}^{ii}$ once more, instead of considering pairs $(a0,a1),(a1,a2)$ (and $(a0,a2)$) in a relation, we can also consider such a pair as an edge, which is topology.

A structure where both vertices of an edge have the same colour would no longer be a chromatic simplicial complex, where in any simplex all vertices must have different colours. We tentatively call complexes where the $\chi$ map may assign the same colour to more than one vertex in a simplex a polychromatic simplicial complex.

Starting out with edges $\{a0,a1\}$ and $\{a0,a1\}$ in the model ${𝒞}^{iii}$ we would get the model ${𝒞}^{vi}$ as below.

This model ${𝒞}^{vi}$ allows for additional epistemic notions, using the novel topological information. For example, reminiscent of the plausibility order (but also essentially different, as we will see) consider the shortest $a$-path linking vertices. Given $a0$, $a1$ is one step away, and $a2$ is two steps away. Based on that, and somewhat dual to the prior ${𝒞}^{iii}$, we can interpret this as agent $a$ considering $a0$ its most plausible local state, $a1$ less, and $a2$ least (the dual where $a2$ is most and $a0$ least plausible from the perspective of $a0$ seems less intuitive in this interpretation). Similarly we can order facets that way, from the perspective of a given agent $a$, where the distance between facets is the length of the shortest $a$-path between them. We now interpret $B_a\phi$ as before, as truth in the most plausible facet or vertex.

Note that there is a difference with the previous semantics for total $\le$ (and ${\le }_a$) orders: the truth of $B_a\phi$ depends on the actual facet. This is unlike the notions of belief and knowledge employing plausibility models in the previous subsection. These are subjective notions that do not depend on the actual point of evaluation (however, unlike strong belief, that is an ‘objective’ notion as well, that is, a notion depending on the point of evaluation given an equivalence class for an agent).

In model ${𝒞}^{vi}$ we would now have that ${𝒞}^{vi},X\vDash B_a{0}_c$, whereas ${𝒞}^{vi},Y\vDash B_a{1}_b$, and ${𝒞}^{vi},Z\vDash B_a{2}_b$ (where all these are distinguishing formulas in the model, that is, only true in those facets and in none other).

If we let pair $(a0,a2)$ in (relation induced by) the belief function count as well, we get this model ${𝒞}^{vii}$ and there seems nothing against considering them as the three edges of a triangle, as in ${𝒞}^{viii}$:

In this more topological interpretation involving simplexes (edges or triangles, here) of vertices with the same colour, we can maybe somehow interpret this as different mental states of the same agent, a structured form of the beliefs the agent considers possible. The representation clearly allows agent $a$ to reason about what her beliefs are in vertex $a0$ as different from what her beliefs are in vertex $a1$, or $a2$. Relations and generalizations to (semi-simplicial sets and) simplicial sets are again conceivable. So far, only semi-simplicial sets have been studied.

It would also be interesting to investigate what happens if we allow higher-dimensional paths, such as the chaining in order to obtain common distributed knowledge [5, 24].

Finally, how can we interpret formulas on simplexes where some but not all vertices are of the same colour, such as the one below?

Another surely fertile direction of research would be to consider models like ${𝒞}^{vii}$ and ${𝒞}^{viii}$ in a neighbourhood semantics [41, 51], a common framework in modal logical semantics although infrequently applied to epistemic notions [9]. Exploring neighbourhood semantics might lead to new insights on coalition logic which found recent application to the specification and verification of smart contracts [52].

In neighbourhood semantics, going into simplicial mode, we would have that $𝒞,X\vDash K_a\phi$ if there is a neighbourhood (a set of facets) of $X$ for agent $a$ such that $\phi$ is true in all the facets in that neighbourhood. Or, possibly more intuitively, given a vertex $v$ with colour $a$, $K_a\phi$ is true in $v$ if there is an $a$-neighbourhood of $v$ where $\phi$ is true.

In ${𝒞}^{vii}$ (or ${𝒞}^{viii}$) facet $W$ has three neighbourhoods for $a$: $\{W,X\}$, $\{Z\}$, and $\{Y\}$. Agents $b$ and $c$ only have a singleton neighbourhood in these structures, we revert to the standard knowledge semantics here. Therefore true in $W$ are: $K_a{0}_c$ (in $\{W,X\}$), $K_a{1}_b$, and $K_a{2}_b$. Observe that these three neighbourhoods do not intersect (there are not any two such that their intersection contains a facet), which, in Kripke semantics, is common fare for neighbourhoods. (In this sort of interpretation, it seems even impossible.) Although all this is crying for an intuitive interpretation, we will leave this as such in this report and instead relay it to further research.

It was agreed upon that before modelling Byzantine agents (that is, unreliable information or malicious intentions), we needed to have a fitting notion of belief. And indeed that occupied the main part of this report. It is clear that, as usual in action model logic, similar structures as presented above for the static notion of belief can be employed to encode dynamic notions involving deceit, error, and Byzantine conduct in general. Indeed, in simplicial semantics the “Kripke-style action models” have natural counterparts as simplicial action models [45, 24]. However, asymmetric versions of that needed for Byzantine communication have not yet been investigated. Additionally, novel update mechanisms such as communication patterns and related [5, 14] could also be contemplated to model Byzantine conduct. The update of simplicial models with communication patterns has been described in [14], including summary suggestions how to represent them as “simplicial communication patterns”. All these horizons seem currently pretty far away, although mouth-watering in their presumed modelling features.

Let us close this far too short subsection on dynamics with a simplicial action model ${𝒞}^x$ representing that agent $c$ dies (that process $c$ crashes), although agents $a$ and $b$ only partially observe that, they remain uncertain about this. The preconditions of all three vertices are $\top$ (the always true proposition). As before, there are two $a$–$b$ edges, the lower edge is a maximal simplex (the complex is an impure simplicial set). If we update a simplicial model with this simplicial action model, any simplex is duplicated into one where $c$ is alive and a for $a$ and $b$ indistinguishable one where $c$ is dead. Even more elementary, simplicial action model ${𝒞}^{xi}$ consists of the $a$–$b$ edge part of ${𝒞}^x$ and models that $c$ is dying, pure and simple. And then, finally, to have at least some Byzantine in the picture, the action ${𝒞}^{xii}$ where $a$ incorrectly believes $c$ to be dying, to the despair of $b$ and, obviously, $c$ who both observe that.