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.
Description:
Dissertation under the supervision of Dr.Sujata Ghosh, Associate Professor, Computer Science Unit,
Indian Statistical Institute, Chennai