Colloquium: Mehrnoosh Sadrzadeh

You are cordially invited to attend the following School of Informatics Colloquium.

Friday, May 1, 2009
3:00 p.m.
LH 102

Mehrnoosh Sadrzadeh, Oxford University, will present, “Aximo: implementation of a decision procedure for information update.”

Abstract:
In scenarios of multi-agent systems, agents communicate with each other to acquire new information. All of us take part in such scenarios when talking, emailing, and bidding or shopping on the net. The complexity of information flow in these scenarios, makes the development of an automated reasoner for them a must. Challenges arise in the closer-to-real-life versions of these scenarios, when the agents are not honest or the communication channel is not safe. These cause misinformation flow and increase the complexity of reasoning. I shall present a syntax and an automated decision procedure for proving epistemic properties of interactive scenarios of multi-agent systems. The novelty of the decision procedure is its use of the categorical rules of adjunction to reduce the epistemic and dynamic modalities. The implementation of the decision procedure, a C++ program called Aximo written by S. Richards, consists of a rewrite system and a recursive reasoner. I go through the termination and complexity of the program, show its soundness with regard to an algebraic axiomatics, and demo its applicability by proving properties of honest and also dishonest versions of the the muddy children puzzle as well as a coin toss scenario. I may hint on how the same procedure can be extended to reason about classical and quantum security protocols.