Date: May 13th 2025, IRIF, Paris

Location: Sophie Germain Building (room 3052) zoom link to virtual meeting

Programme

9:00-9:30 Welcome & project news

9:30-10h20 Romain Delpy (LABRI) : On the send-synchronizability problem for mailbox communication

A system of communicating automata is send-synchronizable if its set of send sequences (i.e., the projection on send actions of its executions) is the same when communications are asynchronous and when they are rendez-vous synchronizations. Send-synchronizability was claimed to be decidable for the mailbox semantics (Basu and Bultan, 2012) and for the peer-to-peer semantics (Basu and Bultan, 2016). Finkel and Lozes showed in 2017 that the proofs of these results are flawed, and they proved that send-synchronizability is in fact undecidable for peer-to-peer systems. The send-synchronizability problem for mailbox systems was left open. A partial solution was recently proposed in (Di Giusto, Laversa and Peters, 2024). In this paper, we revisit the send-synchronizability problem for mailbox systems. Firstly, we show that send-synchronizability is undecidable for mailbox systems, thus closing the question left open in (Finkel and Lozes, 2023) and (Di Giusto, Laversa and Peters, 2024). Secondly, we show that send-synchronizability is decidable for the class of 1-schedulable mailbox systems. A system is 1-schedulable if every execution can be re-scheduled into an equivalent execution where each send is either immediately followed by its matching receive, or is never matched. Despite the apparent similarity between send-synchronizability and 1-schedulability, the proof that send-synchronizability is decidable for 1-schedulable mailbox systems is quite involved. We believe that the techniques that we develop in this proof could be used to address other problems on mailbox systems, such as the realizability problem.

10:20-11:10 Igor Walukiewicz (LABRI) : Partial-order: new lower bounds and heuristics

The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective.

In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to big progress in the field. We ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just write and await instructions. This lower-bound result justifies systematic study of heuristics for stateful partial-order reduction.

We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. We describe a heuristic for the IFS oracle. In our implementation, on many models we get 10x fewer states compared to existing partial-order methods.

11:10-11:30 Coffee break

11:30-12:20 Karine Altisen (VERIMAG) : Revisited Convergence of Dolev et al BFS Spanning Tree Algorithm

We provide a constructive proof for the convergence of Dolev et al’s BFS spanning tree algorithm running under the general assumption of an unfair daemon. Already known proofs of this algorithm are either using non-constructive principles (e.g., proofs by contradiction) or are restricted to less general execution daemons (e.g., weakly fair). In this work, we address these limitations by defining the well-founded orders and potential functions ensuring convergence in the general case. The proof has been fully formalized in PADEC, a Coq-based framework for certification of self-stabilization algorithm.

12:30-14:00 Lunch break

14:00-14:50 Marie Fortin (IRIF) : High-Level Message Sequence Charts: Satisfiability and Realizability Revisited

Message sequence charts (MSCs) visually represent interactions in distributed systems that communicate through FIFO channels. High-level MSCs (HMSCs) extend MSCs with choice, concatenation, and iteration, allowing for the specification of complex behaviors. We revisit two classical problems for HMSCs: satisfiability and realizability. Satisfiability (also known as reachability or nonemptiness) asks whether there exists a path in the HMSC that gives rise to a valid behavior. Realizability concerns translating HMSCs into communicating finite-state machines to ensure correct system implementations.

While most positive results assume bounded channels, we introduce a class of HMSCs that allows for unbounded channels while maintaining effective implementations. On the other hand, we show that the corresponding satisfiability problem is still undecidable.

This is based on joint work with Benedikt Bollig and Paul Gastin.

14:50-15:40 Neven Villani (VERIMAG) : Verifying Parameterized Networks Specified by Vertex-Replacement Graph Grammars

We consider the parametric reachability problem (PRP) for families of networks described by vertex-replacement (VR) graph grammars, where network nodes run replicas of finite-state processes that communicate via binary handshaking. We show that the PRP problem for VR grammars can be effectively reduced to the PRP problem for hyperedge-replacement (HR) grammars, at the cost of introducing extra edges for routing messages. This transformation is motivated by the existence of several parametric verification techniques for families of networks specified by HR grammars, or similar inductive formalisms. Our reduction enables applying the verification techniques for HR systems to systems with dense architectures, such as user-specified cliques and multi-partite graphs.

15:40-16:10 Corto Mascle (MPI-SWS) : Parameterised flows and parameterised MDPs

In 2020, Colcombet, Fijalkow and Ohlmann introduced the Sequential Flow Problem, as an essential tool for the control of parameterised Markov decision processes. It takes as input a graph and a set of capacity functions, and asks whether we can transfer arbitrarily many tokens from a state to another in a sequence of steps that all satisfy at least one of the capacity constraints. We present a new solution to this problem, inspired by Simon’s proof that boundedness is decidable for distance automata. We will then review the connection between this problem and the parameterised MDP model.