Abstracts

Some new developments in epistemic simplicial semantics

Slides

I will present some recent work and ideas in epistemic simplicial semantics, basically: (i) different three-valued weak Kleene semantics for impure complexes (furthering recent PhD work by Rojo Randrianomentsoa & Prague collaborators), (ii) recent work by Yuanzhe Yang (presented at TARK) using term-modal logic to unify two-valued and three-valued epistemic simplicial semantics, (iii) using oriented complexes for a local (face, not facet interpretation) semantics of belief and related epistemic notions (collaborative work with Bern).

Hypergraph Semantics for Doxastic Logics

Slides

We present a new semantics for logics of belief. Our semantics 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 for epistemic logic, while accounting not only for knowledge, but also for belief. We provide systems of both consistent and inconsistent belief. To establish the completeness of our axiomatizations, we introduce canonical hypergraph models. In addition to that, we present direct conversions between doxastic Kripke models and directed hypergraph models

Simplicial Belief

Slides

Recently, much work has been carried out to study simplicial interpretations of modal logic. While notions of (distributed) knowledge have been well investigated in this context, it has been open how to model belief in simplicial models. We introduce polychromatic simplicial complexes, which naturally impose a plausibility relation on states. From this, we can define various notions of belief. We further explore how these complexes are connected to neighborhood semantics.

Preserving Hyperproperties in Programs that Use Concurrent Objects

Abstraction is key to the design and verification of large, complicated software. In concurrent programs, abstraction is often used to encapsulate low-level shared memory accesses within high-level so-called concurrent objects. Concurrent object implementations are often related to atomic specifications, where operations take place instantaneously, via the famous linearizability condition. A key benefit of linearizability is that reasoning about trace properties of programs using concurrent objects can be simplified by replacing them with their atomic specifications.

Unfortunately, linearizability does not preserve so-called hyperproperties which characterize sets of traces, eg., security properties like noninterference or probabilistic guarantees of randomized programs. A more restrictive property, strong linearizability, does preserve hyperproperties but it is impossible to achieve in many situations. In this talk, I will present various results concerning the relationship between strong linearizability and classic formal verification techniques like forward simulations, and results concerning the implementability of strong linearizability.

Space-Time Trade-off in Bounded Iterated Memory

Slides

The celebrated asynchronous computability theorem (ACT) characterizes tasks solvable in the read-write shared-memory model using the unbounded full-information protocol, where in every round of computation, each process shares its complete knowledge of the system with the other processes. Therefore, ACT assumes shared-memory variables of unbounded capacity. It has been recently shown that boundedvariables can achieve the same computational power at the expense of extra rounds. However, the exact relationship between the bit capacity of the shared memory and the number of rounds required in order to implement one round of the full-information protocol remained unknown. In this paper, we focus on the asymptotic round complexity of bounded iterated shared-memory algorithms that simulate, up to isomorphism, the unbounded full-information protocol. We relate the round complexity to the number of processes n, the number of iterations of the full information protocol r, and the bit size per shared-memory entry b. By analyzing the corresponding protocol complex, a combinatorial structure representing reachable states, we derive necessary conditions and present a bounded full-information algorithm tailored to the bits available b per shared memory entry. We show that for 

n>2, the round complexity required to implement the full-information protocol satisfies Ω((n!)r−1⋅2n−b). Our results apply to a range of iterated shared-memory models, from regular read-write registers to atomic and immediate snapshots. Moreover, our bounded full-information algorithm is asymptotically optimal for the iterated collect model and within a linear factor n of optimal for the snapshot-based models.

Link: (https://arxiv.org/pdf/2509.13157). 

Mixing decentralized systems with probabilities

Slides

Various kinds of Markov processes are used for modeling probabilistic systems: Markov decision processes (MDPs) are used when an agent can react in a fully observable environment, partially observable MDPs (POMDPs) describe systems in which an agent has to deal with uncertainty about the current state. The study of these models has been a cornerstone of AI and control theory research for over 70 years. 

For multi-agent systems, the natural extension is the Decentralized POMDP (Dec-POMDP). This framework models a team of cooperative agents, each receiving its own local observations, who must coordinate their actions to optimize a shared objective. The decentralized nature of information makes finding optimal strategies notoriously difficult, but it provides a versatile setting for analyzing problems in distributed computing, robotics, and economics.

We’ll discuss the main results in this field, how to model the standard examples of distributed systems in this setting, and possible connections with geometry and simplicial structures. 

What are Your Powers? (Truth Set Algebras)

Slides

I will present a logic with modalities representing four different types of multistep strategies in the imperfect information setting, depending on an agent's memory ability and observational ability. I will discuss the connections between the four modalities, using a new ``truth set algebra'' technique for proving undefinability, which is significantly different from the existing techniques based on bisimulation. The newly proposed technique is used to prove the undefinability of each of the four modalities through a combination of the three others. 

Probabilistic methods in distributed computing

Slides.

I will present the following results to appear in DISC 2025 (with Pierre Fraigniaud and Boaz Patt-Shamir), and time permitting, discuss other randomized problems that have been studied in distributed computing.

We consider a stochastic network model consisting of a set of n synchronous processes communicating by message passing. In each round, processes send messages directly to each other over a complete communication graph. The processes do not fail, but messages can be lost. Each message is delivered with probability p, for a given parameter p ∈[0,1]. We study the following optimization version of approximate agreement in this model. We assume that processes start with binary input values, execute an algorithm for a fixed number of rounds, and decide values in [0,1] satisfying the usual validity requirement stating that if all processes start with the same input value, then they should all decide that value. We propose deterministic algorithms that minimize the expected discrepancy, namely, the expected maximum distance between the decided values. We also present lower bounds on the expected discrepancy, which demonstrate the optimality of our algorithms for two processes. Finally, we present applications of our algorithms to solve randomized consensus and randomized approximate agreement.

Virtual Group Knowledge and Group Belief in Topological Evidence Models

We study notions of (virtual) group knowledge and group belief within multi-agent evidence models, obtained by extending the topological semantics of evidence-based belief and fallible knowledge from individuals to groups. We completely axiomatize and show the decidability of the logic of (``hard'' and ``soft'') group evidence, and do the same for an especially interesting fragment of it: the logic of group knowledge and group belief. We also extend these languages with dynamic evidence-sharing operators, and completely axiomatize the corresponding logics, showing that they are co-expressive with their static bases.