MCMAS is a model checking system for multi-agent systems. It allows model checking of temporal, epistemic, deontic, and cooperative properties of systems to be investigated. The input language of MCMAS is based on "interpreted systems", a very low-level representation of multi-agent systems based on the interpreted systems model described in Chapter 4 of Fagin, Halpern, Moses, and Vardi's book "Reasoning about Knowledge". This representation is very low-level: it basically involves thinking of a system almost at the level of automata. The aim of this project is to take the source code for MCMAS, and adapt it for a higher-level representation: the Simple Reactive Modules Language language (SRML), a (very) simplified version of Alur and Henzinger's Reactive Modules language. SRML is described in a paper by Hoek, Lomuscio, and Wooldridge.
The logic of knowledge (epistemic logic) is a formalism that is intended to enable reasoning about what agents in a multiagent system know. The semantics of epistemic logic are given in terms of "possible worlds". For example, if I thought that there was one possible world (state of affairs) where it was raining in Liverpool, and another where it was not raining in Liverpool, then you would say I did not know whether or not it was raining in Liverpool. If, however, in all the states of affairs that I considered possible, it was raining in Manchester, then according to possible worlds semantics, you would say I knew it was raining in Manchester. The idea of this project is to develop a graphical tool for drawing these knowledge structures pictorially, and then for checking whether or properties are true in these structures.
Main reference: R.Fagin, J.Y.Halpern, Y.Moses, and M.Y.Vardi. Reasoning About Knowledge MIT Press 1995.