Modal logics for communicating rule-based agents

In this paper, we show how to establish correctness and time bounds (e.g., quality of service guarantees) for multi-agent systems composed of communicating rule-based agents. The formal models of multi-agent systems we study are transition systems where each transition corresponds to either a rule firing or an act of communication by an agent. We present a complete and sound modal logic which formalises how the beliefs of communicating rule-based agents change over time. Using a simple example, we show how this logic can be used to specify temporal properties of belief change in multi-agent systems in a precise and realistic way, and how existing modal logic techniques such as model-checking can be used to state and verify properties of agents.