Aximo: implementation of a decision procedure for information update

by Mehrnoosh Sadrzadeh

Oxford University Computing Laboratory

Date

Friday, May 1, 2009

Time

3:00 p.m. — 4:00 p.m.

Place

Lindley Hall 102

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.

Biography: Mehrnoosh Sadrzadeh is an EPSRC postdoctoral research fellow of Oxford University Computing Laboratory and a Research Fellow of Wolfson College. She has been lecturing for the course Logic of Multi-Agent Information Flow and running the Oxford Advanced Seminar on Informatic Structures, founded by S. Abramsky. In her Ph.D. thesis jointly supervised by Prof. M. Marion in Montreal and A. Baltag in Oxford, she developed the first algebraic model of information update. Her model offered simple semi-automatic proofs of challenging multi-agent scenarios and was later implemented in a C++ program, serving as the only automated proof-theoretic tool for the field of Dynamic Epistemic Logic. Currently, she is actively working on further implementations of the algebra, extending it with probabilities, and applying it to reasoning about security and Quantum security protocols; collaborating with Dyckhoff, Panangaden, and Pucella. She is also working on algebraic models of natural languages and the interface between vector space models and logical models of language. Her recent work in collaboration with Lambek, Pulman, Clark and Coecke, has led to a solution to an open problem of the field of computational linguistics.

Colloquium Provided By:

the School of Informatics