Fibred belief logic for multi-agent systems

Multi-agent systems consist of a number of autonomous agents (software programs) that are capable of independent action on behalf of their users. Agents communicate with one another by exchanging messages, and they have the ability to co-operate, co-ordinate and negotiate with each other to achieve their objectives. In order to develop theories to specify and reason about various aspects of multi-agent systems, many researchers have proposed the use of modal logics such as belief logics, logics of knowledge, and logics of norms. As multi-agent systems operate in dynamic environments, there is also a need to model the evolution of multi-agent systems through time. In order to introduce a temporal dimension to a belief logic, we consider a powerful technique called fibring for combining belief logics and temporal logics. In a fibred belief logic, both temporal operators and belief operators are treated equally. This paper in particular discusses a combination of a belief logic called Typed-Modal Logic with a linear-time temporal logic. We show that, in the resulting logic, we can specify and reason about not only agents’ beliefs but also the timing properties of a system. With this logical system one is able to build theories of trust for the description of, and reasoning about, multi-agent systems.