What is Model Checking Problem

It becomes evident in recent years a surge of interest to applications of modal logics for specification and validation of complex systems. It holds in particular for combined logics of knowledge, time and actions for reasoning about multiagent systems (Dixon, Nalon & Fisher, 2004; Fagin, Halpern, Moses & Vardi, 1995; Halpern & Vardi, 1986; Halpern, van der Meyden & Vardi, 2004; van der Hoek & Wooldridge, 2002; Lomuscio, & Penczek, W., 2003; van der Meyden & Shilov, 1999; Shilov, Garanina & Choe, 2006; Wooldridge, 2002). In the next paragraph we explain what are logics of knowledge, time and actions from a viewpoint of mathematicians and philosophers. It provides us a historic perspective and a scientific context for these logics. For mathematicians and philosophers logics of actions, time, and knowledge can be introduced in few sentences. A logic of actions (ex., Elementary Propositional Dynamic Logic (Harel, Kozen & Tiuryn, 2000)) is a polymodal variant of a basic modal logic K (Bull & Segerberg, 2001) to be interpreted over arbitrary Kripke models. A logic of time (ex., Linear Temporal Logic (Emerson, 1990)) is a modal logic with a number of modalities that correspond to “next time”, “always”, “sometimes”, and “until” to be interpreted in Kripke models over partial orders (discrete linear orders for LTL in particular). Finally, a logic of knowledge or epistemic logic (ex., Propositional Logic of Knowledge (Fagin, Halpern, Moses & Vardi, 1995; Rescher, 2005)) is a polymodal variant of another basic modal logic S5 (Bull & Segerberg, 2001) to be interpreted over Kripke models where all binary relations are equivalences.