StFX Logic Talk 2: Model Checking Knowledge Dynamics of Multi-Agent Systems

Abstract:

In this talk, I will first briefly introduce Model Checking and Multi-Agent Systems (MAS), then focus on two frameworks on modelling knowledge dynamics of MAS. The first is Dynamic Epistemic Logic, which is reasoning about knowledge and actions, and the second is Temporal Epistemic Logic, which is reasoning about knowledge and time. Then I will give a comparison of three state-of-the-art model checkers for MAS (DEMO, MCK and MCMAS) by verifying a communication protocol for Russian Cards Problem. Finally I will discuss with the audience about the possible ways of modelling the interactions in Health Care Services & Work-flows.

(Some work was jointly done with H.P van Ditmarsch, W. van der Hoek, and R. van der Meyden)

References:

• Chapter 6 of my PhD Thesis.

This Russian Cards Problem originated at the Moscow Math Olympiad 2000. Maybe you could try to solve it before the talk.

From a pack of seven known cards two players each draw three cards and a third player gets the remaining card. How can the players with three cards openly inform each other about their cards, without the third player learning from any of their cards who holds it?