The purpose of this paper is to integrate a number of ideas from knowledge representation, with ideas from the semantics of programming language, m 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, makes inference 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 w 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.