Formal models are magic
Speaker: 
Laure PETRUCCI
Professor
University Paris 13
| Date: Time: Venue: | | 1 December 2026, Tuesday 10:00am – 11:00am School of Computing & Information Systems 1 (SCIS 1)
Level 4, Meeting Room 4-4
Singapore Management University
Singapore 178902
Please register by 30 November 2026 
|
|
About the Talk
In this work, we investigate a variant of the Four Glasses Puzzle (FGP) through the lens of formal verification. Although the puzzle appears to be unsolvable at first glance, formal verification enables the discovery of a correct solution. We demonstrate how the model can be constructed and reduced through progressive abstractions, ultimately yielding a concise and comprehensible model that captures all possible puzzle configurations. To ensure computational efficiency, we introduce the Escape Game - an algorithmic construction that eliminates redundant cycles and facilitates strategy synthesis under imperfect information. Finally, by analysing the strategic capabilities of the player, we present a solution to the puzzle. The approach is formally defined and proven correct.
About the Speaker
Laure PETRUCCI obtained her PhD in Computer Science from University Paris 6 in 1991. She then became associate professor in Evry. In 2003, she obtained a Full Professor position at University Paris 13. Her research takes place in the SAFER team of the LIPN laboratory. Her area of expertise is formal specification and verification of concurrent systems so as to guarantee their appropriate behaviour, using automata or Petri nets models, as well as parametric models. In order to tackle the well-known state space explosion problem, the research she develops exploits modularity in the models, proposes distributed approaches, and algorithms for parameter synthesis. In recent works she has tackled strategy synthesis for multi-agent systems, according to different semantics, and proposed novel logics to express properties and model-checking approaches.
