Abstracts

Implementability of Concurrent Objects from a Topological Perspective

Slides

Since the early 90s, a number of combinatorial and algebraic topology techniques have been successfully applied to distributed computing, which has resulted in a rich and solid computability theory of distributed computing. However, the theory has mostly been applied to study distributed problems that can be defined through the task formalism. Roughly speaking, a task is the equivalent of a function in a distributed setting. Very little is known about topology techniques applied to distributed problems that cannot be specified as tasks. A prominent example are concurrent objects, which are of great interest in the design of real-world systems, for example, linearizable concurrent data structures. In this talk I will present work in progress that attempts to extend the theory to encompass this type of distributed problems. 

Local Semantics for Simplicial Models

Slides

We present a doxastic, relational variant of the simplicial model, which comes with a local semantics. That is, formulas are evaluated not just on global worlds, but on local states and arbitrary sets of local states. Simplicial models already make the local states of agents explicit as the core elements of which a global state is composed. The accessibility relation, however, is defined between global states. Thus, in order to compute Alice's beliefs about Bob's local state, we need to look at the entire global states that Alice considers possible. On our models, we instead define an accessibility relation directly between local states. Alice’s possible worlds are now merely collections of local states that Alice considers possible. This results in an interesting three-valued semantics that (superficially) resembles the semantics on impure simplicial complexes in Randrianomentsoa et al. (2023), but comes with radically different validities. 

Hypergraph Semantics for Modal Logics: Axiomatizations and Limitations

Slides

Recent years have seen the emergence of simplicial semantics for various systems of multi-agent epistemic logic. In contrast to relational models, the primary building blocks of simplicial models are not possible worlds (i.e., global states of the system), but local states of agents. Recently, a more general semantics has been developed that is based on directed hypergraphs, a generalization of ordinary directed graphs in which edges are able to connect more than two vertices. Directed hypergraph models preserve the characteristic features of simplicial models (such as their geometric nature and the precedence of local states over global states), but also allow to account for the beliefs of agents. So far, however, only a specific notion of accessibility between global states in directed hypergraph models has been considered. In the talk, we investigate a large class of accessibility relations for hypergraph models and provide sound and complete axiomatizations for the resulting logics. We also identify certain limitations of the general framework: various logics of interest do not allow for a "natural" hypergraph semantics

Characterizing Stabilizing Consensus Topologically and Epistemically

A classic result in the epistemic analysis of distributed systems is the equivalence of terminating consensus and common knowledge. Originally established for simultaneous consensus only, Gonczarowski and Moses have recently shown how to overcome the fundamental ``Halpern-Moses Paradox'', which inevitably arises in systems with timing uncertainties and plagued attempts to establish an analogous result for non-simultaneous consensus.

    In this presentation we present results from our recent paper where we build on, and non-trivially extend the latter approach to establish the very first necessary and sufficient epistemic conditions for solving stabilizing consensus. Stabilizing consensus is a non-terminating variant of consensus, where agents may change their decision value finitely often before eventually stabilizing on a common value. Since it is a weaker problem than terminating consensus, stabilizing consensus can be solved in systems where the latter is unsolvable. Our results reveal that, in order to solve stabilizing consensus, agents need to establish a novel notion of common knowledge, called common foreknowledge. Moreover, we show that our epistemic characterizations of both terminating and stabilizing consensus correspond one-to-one to the respective topological characterizations. We achieve this by establishing a novel connection between the knowledge defined on the points of the runs-and-systems framework and the point-set topology defined directly on the set of runs: Dynamic common knowledge, as defined by Gonczarowski and Moses, holds in (and requires) clopen sets and our novel common foreknowledge holds in (and requires) semi-open sets.

Heterogeneous Bracha Broadcast

A distributed protocol is heterogeneous when different participants may have different trust models, i.e. when multiple notions of "quorum" are used in the protocol.  Heterogeneous systems arise naturally when considering interaction of distinct homogeneous protocols, e.g. a cross-chain or cross-bank payment, or any other communication of two distributed systems. 

It is difficult to get this right, and ad hoc solutions have a way of translating directly into inconvenience in a user's real-life experience of using practical systems. 

I will report on the design of a mathematically principled heterogeneous generalisation of Bracha Broadcast, which was designed as a template for practical use.

Technical innovations are: 

1. Declarative protocol design.  We separate the logical content of the protocol from its algorithmic realisation.

2. History structures.  To make heterogeneity work, it turns out to be necessary for participants in the protocol to reason about what other participants know or believe (because behaviour must be judged correct or incorrect in terms of a local trust model rather than any homogeneous universally-known one).  A novel notion of time similar to the von Neumann cumulative hierarchy model of set theory, which we call history structures, delivers a useful mathematical model.

3. Modal logic based on semitopologies.  We use a novel modal logic which includes modalities based on semitopologies, to declaratively specify and reason about quorums and quorum-intersections.

I will give a rigorous but approachable outline of the broad and deep body of mathematics which was required to address this challenge.  The interested reader can find out more in the following resources:

* The Heterogeneous Bracha Broadcast paper (submitted)  https://doi.org/10.5281/zenodo.17611735  and its Lean formalisation  https://zenodo.org/records/17611735

* The Semitopology book  https://www.amazon.co.uk/Semitopology-Decentralised-Collaborative-Topology-Algebra/dp/1848904657

* The Declarative Bracha Broadcast paper   https://arxiv.org/pdf/2512.21137.

How groups communicate - variations in (a)synchronicity and models

There are several ways for agents in a group to communicate, that do not always result in distributed knowledge becoming common knowledge. One is by publicly sharing all they know, via intersecting the accessibility relations of all the agents in the group. After such a resolution, agents involved in the sharing all have the same knowledge. Whether it is common knowledge that this resolution took place - for both agents in the group and agents outside the group - depends on whether we assume (a)synchronicity. Ågotnes and Wang’s Resolving Distributed Knowledge enforces synchronicity: group resolutions are public in the sense that all agents - either involved in the sharing or outside the group - are aware of such events. Things become more complex with asynchrony, where agents not involved in the sharing are not aware that a resolution event has occurred. In recent work (in press), we have proposed a semantics for resolving such asynchronous distributed knowledge, where agents cannot distinguish between sequences of resolution events of possibly different length. We will present the asynchronous semantics and compare them to the synchronous semantics. Resolution events are examples of so-called communication patterns formalizing communication in distributed systems. Finally, we will show how we interpret resolution and communication patterns on simplicial complexes, using the correspondence between Kripke semantics and simplicial semantics.

Joint talk with Hans van Ditmarsch, partially based on:

Philippe Balbiani, Hans van Ditmarsch, Clara Lerouvillois, Resolving Asynchronous Distributed Knowledge, Proceedings of Advances in Modal Logic 2026, to appear.

Dynamic Common Knowledge and Agreement

This works shows the connection between the recently introduced notion of Dynamic common knowledge and All-or-nothing agreement problems,  a wide class of agreement problems that includes Consensus, Reliable broadcast, and Atomic commitment. This connection allows for an abstract and model-independent characterization of agreement problems. In particular, it can be used to simplify and/or optimize agreement protocols in a rigorous fashion. The talk is based on joint work with Or David.

Properly confused about properness!

A (partial) epistemic frame is said to be proper if any two states can be distinguished by at least one (alive) agent. This condition has proven useful in analyzing the correspondences between relational frames and simplicial models across various epistemic logics, yet its implications remain somewhat underexplored. In this talk, I will discuss some aspects of properness, focusing in particular on phenomena that arise in the setting of three-valued epistemic logic on impure simplicial complexes.

Tool-Supported Action Model Synthesis for Truly Private Model Updates

Epistemic logic has been successfully applied to modeling of epistemic and doxastic attitudes of agents in distributed systems. Dynamic Epistemic Logic (DEL) adds communication via mode transformation updates. Since agents in distributed systems often exchange information without other agents knowing about it, however, the inherent assumption that agents possess common knowledge of the model is generally not adequate when describing fully private communication.

In this talk, I will present the following results of my forthcoming PhD thesis, which addresses this deficiency:

1) A slight variation of standard action models enriched by a new idea of postcondition.

2) A novel synthesis procedure that, based on a goal formula, generates a pointed action model s.t. when this action model is applied to a pointed epistemic model, the goal formula holds at the point of the epistemic model (given some assumptions), without introducing new unrelated beliefs and preserving consistency of agents' beliefs as much as possible.

The many technical statements and proofs I encountered in the course of my PhD work suggested to use an epistemic model checker for verifying their correctness. As none of the (few) existing tools provided the features I needed, I decided some years ago to develop my own high-performance epistemic model checking and visualization tool. Whereas it is still work in progress, it already supports the model synthesis approach described above. I will hence complement the first part of my talk with a live demo of my model checking and visualization tool.

An Implementation of Belief Revision in Simplicial Models for Dynamic Epistemic Logic

In this talk we set out to show how to connect belief revision to dynamic epistemic logic by leveraging tools given by the setting of simplicial semantics. We start by modifying some of the existing models for DEL in simplicial semantics ("Knowledge and Simplicial Complexes", "A Simplicial Complex Model for Dynamic Epistemic Logic"). In particular, we will show how to modify these models for DEL so that they work in a setting for belief, rather than knowledge, using tools from the upcoming paper "Belief In Simplicial Complexes". With this in hand, we will then motivate an endogenous notion of "nearness" between facets, where two facets sharing more perspectives in common is interpreted as the two facets being more similar. We exploit this notion of "nearness" to give a model for belief revision ala Lewis' "Probabilities of Conditionals and Conditional Probabilities", and ultimately we use this notion of nearness to give a model of DEL where agents update via revision, rather than classically. We will conclude with a discussion of some existing and future work which attempts to exploit this notion of nearness to give new tools for fault tolerance.