(Note the unusual schedule)
Venue: Institut Mines-Télécom, Palaiseau, salle 4A485
10:30 Dylan Bellier (present), Télécom SudParis:
Plan Logic and "efficient" strategic reasoning
► Abstract:
When reasoning about games, one is often interested in verifying more intricate strategic properties than the mere existence of a winning strategy for a given coalition. Several languages, among which the very expressive Strategy Logic (SL), have been proposed that explicitly quantify over strategies in order to express and verify such properties. However, quantifying over strategies poses serious issues: not only does this lead to a non-elementary model-checking problem, but the classic Tarskian semantics is not fully adequate, both from a conceptual and practical viewpoint, since it does not guarantee the realisability of the strategies involved.
In this presentation, I present a different approach and introduce Plan Logic (PL), a logic that takes plans, i.e., sequences of actions, as first-class citizens instead of strategies. Since plans are much simpler objects than strategies, it becomes easier to enforce realisability. In this setting, we can recover strategic reasoning by means of a compositional hyperteams semantics, inspired by the well-known team semantics. We show that the Conjunctive-Goal and Disjunctive-Goal fragments of SL are captured by PL, with an effective polynomial translation. This result relies on the definition of a suitable game-theoretic semantics for the two fragments.
11:15 Discussion
12:00 Lunch
13:30 Jamie Gabbay (online), Heriot-Watt University, Edinburgh:
Declarative distributed broadcast using three-valued modal logic and semitopologies
► Abstract:
Distributed algorithms are notoriously difficult to design, understand, and prove correct. Most distributed protocols (e.g. broadcast or consensus) are in practice specified in pseudocode, and verified in informal reasoning or using a linear temporal logic. This means that the underlying programming paradigm is imperative, and therefore proofs tend to be relatively involved, detailed and complicated, as one would expect for verifying an imperative process.
I've developed a declarative axiomatic approach based on three-valued modal logic and semitopologies. Operational details (including details of message-passing and their ordering) are elided. The result feels much more high level, akin to declarative programming. Specifications and correctness proofs come out correspondingly simpler and can mostly proceed by compact and precise abstract symbol-pushing.
This approach has been battle-tested on textbook algorithms and on industrial protocols, and it has been successfully used to locate and correct defects in real-life industrial protocols (and indeed, in my case, to understand them!). I will give an overview of the basic ideas and principles.
The interested reader can find out more here:
https://doi.org/10.1093/logcom/exae050 (semitopologies)
https://arxiv.org/pdf/2502.00892 (declarative Paxos)
https://arxiv.org/pdf/2512.21137 (declarative Bracha broadcast)
semitopology book
14:15 Discussion & workgroups