TITLE: Verifying Secret Santa and the Dining Cryptographers: how to reason about knowledge, correct behaviour and strategies using extensions of temporal logics
SPEAKER:  Franco Raimondi (School of EIS, Middlesex University)

ABSTRACT:

In this talk I will introduce an extension of the traditional temporal-only symbolic model checking procedures to the verification of knowledge, correct behaviour, and strategies. These modalities are often used to express in a natural way requirements of both hardware and software  systems. Using a number of examples, I will present theoretical results and the features of a newly released tool to support this kind of analysis, simulations and graphical counter-example generation.