LIRa session: Malvin Gattinger

Speaker: Malvin Gattinger (ILLC, University of Amsterdam)

Date and Time: Thursday, April 9th 2026, 15:30-17:00
(Please note the earlier-than-usual time.)

Venue: ILLC Seminar Room F1.15, Science Park 107 and online.

Title: Do you know if the road is still there? Sabotage Modal Logic with Knowledge.

Abstract. Sabotage Modal Logic (SML), originally proposed by Johan van Benthem, is concerned with a two-player game between traveller and demon played on a graph: traveller wants to get from A to B, but demon may delete edges between nodes. Formally, the traveller is modelled by a standard diamond modality whereas the demon is a dynamic modality that deletes edges. Different versions of the resulting logic have been studied in the literature.

In this talk I will describe ongoing work where we add a third modality: the knowledge of the traveller. The resulting language we call SML+K and it can express sentences such as “After any two deletions the traveller still knows that there is a three-step path to the goal”. Or “There is a deletion after which there still is a three-step path to the goal but the traveller will no longer know that there is such a path.”

We developed two semantics for SML+K, one where the knowledge is encoded by an equivalence relation between histories and one where the traveller only stores a set of graphs currently considered possible. At first sight only one of these semantics seems to have perfect-recall, but we actually aim to show that they are equivalent.

For both semantics I will also present a Lean formalization that can also be used as a model checker.

This is joint work with Sujata Ghosh and Saptarshi Sahoo (both Chennai).