Date: October 13th 2026, IRIF, Paris

Location: Sophie Germain Building (room TBA)

Programme

9:00-9:50 Lucie Guillou (IRIF) : Beep is All you need

Stone age networks and beep protocols are minimalist models of distributed computing in which anonymous processes interact using weak communication primitives. Beep protocols are synchronous models where processes are arranged on a graph and are capable of communicating by only sending a single message called a beep. In each round, a process can only distinguish between silence (no beeps from its neighbors) and a beep (at least one beep from its neighbors). Stone age networks are a slightly more powerful model where processes can send messages from a finite alphabet. However, just like beep protocols, each process can only identify the set of messages that is has received from its neighbours, and cannot count how many neighbours sent messages. Despite these severe restrictions, such models have proved expressive enough to capture non-trivial distributed tasks. In this talk, I will present a work on anonymous networks of identical finite-state processes executing stone age and beep protocols over arbitrary communication topologies. We study the state-coverability problem (that is, deciding whether there exists a network topology in which some process can eventually reach a given control state). We first show that both models are equivalent with respect to the state-coverability problem, and then prove that state-coverability on arbitrary topologies reduces to state-coverability on trees. Our main result then establishes that the state-coverability problem is undecidable. Motivated by this undecidability result, we study these networks over restricted classes of topologies and obtain tight complexity results: We show that when restricted to trees of bounded depth, the problem becomes TOWER-complete, while restricting to cliques makes the problem PSPACE-complete. This is a joint work with A.R. Balasubramanian.

9:50-10:40 Ocan Sankur (IRISA) : (Towards) Quantitative Verification with Neural Certificates

10:40-11:10 Coffee break

11:10-12:00 Igor Walukiewicz (LABRI) : Commutations everywhere, using POR without predefined independence of actions

12:00-13:30 Lunch break

13:30-14:20 Nathalie Bertrand (IRISA) : Parameterized Verification of Asynchronous Round-Based Distributed Algorithms via Reduction to Finite-Counter Systems

Traditional model-checking techniques typically verify distributed algorithms only for a fixed number of finite-state processes. Parameterized model checking generalizes this to any number of processes, while still typically assuming that each process is finite-state. In this work, we consider asynchronous round-based distributed algorithms in which each process is infinite-state since it can execute for an infinite number of rounds. We show that the parameterized verification problem for asynchronous round-based distributed algorithms is undecidable, already for simple specifications. Nevertheless, as our main contribution, we provide a reduction to LTL model checking over finite-counter systems and prove that it is sound and complete. This enables the use of off-the-shelf, mature symbolic model checkers for finite-counter systems. We demonstrate the practical applicability of this reduction by verifying safety and liveness properties of several asynchronous round-based consensus and leader-election algorithms using the nuXmv model checker. Joint work with Pranav Ghorpade and Sasha Rubin

14:20-15:10 Neven Villani (VERIMAG) : Reachability by Token Sliding in Parameterized Graphs

In the standard problem of reconfiguration by token sliding, a fixed number of tokens are placed on vertices of a graph, and a move consists of sliding a token along a path that does not contain any other tokens. The task is to decide if a target configuration is reachable from a given initial configuration. Several variations exist to the problem, notably whether or not the support graph is directed (if so, tokens can slide only along oriented edges, otherwise every move is reversible), and whether or not the tokens are distinguishable (if so, the initial and target configurations impose which specific token should be on a given vertex, otherwise only the presence of any token is required). Our focus is on the version with both directed edges and distinguished tokens, which is a generalization of all other cases, but is much less understood.

Our main contribution is to exhibit a cutoff: we prove that a target configuration is reachable if and only if it is reachable within a number of moves that depends only on the number of tokens, independently of the size of the graph. This bound is a single exponential of the number of tokens. The proof is based on successive decompositions of a graph, by viewing an arbitrary graph as first an acyclic graph of strongly connected components, and then further decomposing every strongly connected components into trees of segments of cycles. For each of these successive layers we prove properties of the graph of local configurations, in order to prove a global bound on the diameter of the graph of all configurations.

As one possible application of this result, we show that due to the boundedness of the diameter of the configuration graph, a solution to the problem can be expressed in the Monadic Second Order Logic for graphs. This has consequences for the decidability of the reachability problem in parameterized settings.

15:10-15:40 Coffee break

15:40-16:30 Christoffer Lind Andersen (VERIMAG) : Safety Analysis in Broadcast Networks Defined by Graph Grammars

We consider families of networks where processes communicate by synchronous broadcast (i.e., a sent message is received by all the neighbours of the emitter) and we study the following safety problem: is there a network in the given family, such that some process can reach an error location? Specifically, we focus on families of network topologies defined by graph grammars, where each node of the produced graph can be either a clique or a cloud (anti-clique) of processes of unbounded sizes. We show that, in general, the considered safety problem is undecidable, when the communication is reliable, and becomes decidable with unreliable communication (i.e., broadcast messages can be lost) or whenever the protocols executed by the different processes cannot send and receive messages from the same control state (also known as the wait-only syntactic restriction).