Formal specification of beliefs in multi-agent systems

The formalization of agents attitudes, and belief in particular, has been investigated in the past by the authors of this paper, along two different but related streams. Giunchiglia and Giunchiglia investigate the properties of contexts for the formal specification of agents mutual beliefs, combining extensional specification with (finite) presentation by means of contexts. Cimatti and Serafini address the representational and implementational implications of the use of contexts for representing prepositional attitudes by tackling a paradigmatic case study. The goal of this paper is to show how these two streams are actually complementary, i.e. how the methodology proposed in the former can be successfully applied to formally specify the case study discussed in the latter. In order to achieve this goal, the formal framework is extended to take into account some relevant aspects of the case study, the specification of which is then worked out in detail.