A modal logic for reasoning about belief

The purpose of this paper is to integrate a number of ideas from knowledge representation, with ideas from the semantics of programming language, in a basic logical system for belief. A knowledge-based system can be considered as, in a simplified way, an agent which, based on its current state of information, reasons for purposes such as planning or taking an action that best suits the agent´s goal. There are different ways to formalize such a system. The approach we are taking is model checking: we express an agent´s current state of knowledge by a semantic model, and the agent´s belief or action as some logical formulas. The paradigm of model checking deals with the issue of whether an agent´s current state of knowledge supports an action or a belief. Only supported belief or action are considered as appropriate. This paradigm is, in particular, different from the traditional logical one which represents an agent´s state of knowledge by a set of first-order formulas, and considers a belief or an action appropriate if it happens to be a logical consequence of the set of given formulas