Multi-Agent Systems: Model-checking in Logics of Protocols

Abstract

A multi-agent system can often be described as a protocol based interacting system wherein the information ow, inter-agent communication and agent behavior can be naturally modeled with dynamic and epistemic logics which are di erent variants of modal logics. Such protocols may either be known beforehand to each agent or be unknown to any agent at the start. In the later situation, such protocols are called hidden protocols. When an agent learns of a hidden protocol, it is led to have some expectations about future observations and updates its knowledge of the state by matching its actual observations with the expected ones. In their paper \Hidden Protocols: Modifying our expectations in an evolving world", Hans van Ditmarsch, Sujata Ghosh, Rineke Verbrugge and Yanjing Wang studied how agents perceive such protocols and introduced the notion of epistemic expectation models and a propositional dynamic logic-style epistemic logic, Epistemic Protocol Logic for reasoning about knowledge via matching agents' expectations to their observations, updates of protocols and fact-changing actions. This is of particular interest to modeling scenarios where security aspects mandate knowledge of protocols to be hidden to some or all agents beforehand or at all times. In this project we will focus upon theory and implementation of a model checker for Epistemic Protocol Logic incorporating Epistemic Expectation Models and study formal methods towards a symbolic model checking approach to this end.