Abstract
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.
TopBackground: Modal Logics
All modal logics are languages that are characterized by syntax and semantics. Let us define below a very simple modal logic in this way. This logic is called Elementary Propositional Dynamic Logic (EPDL).
Let true, false be Boolean constants, Prp and Rel be disjoint sets of propositional and relational variable respectively. The syntax of the classical propositional logic consists of formulas which are constructed from propositional variables and Boolean connectives “¬” (negation), “&” (conjunction), “∨” (disjunction), “→” (implication), and “↔” (equivalence) in accordance with the standard rules. EPDL has additional formula constructors, modalities, which are associated with relational variables: if r is a relational variable and φ is a formula of EPDL then
Key Terms in this Chapter
Logic of Actions: A polymodal logic that associate modalities like “always” and “sometimes” with action symbols that are to be interpreted in labeled transition systems by transitions. A so-called Elementary Propositional Dynamic Logic (EPDL) is sample logic of actions.
Perfect Recall Synchronous Environment: An environment for modeling a behavior of a perfect recall synchronous system.
Logic of Knowledge or Epistemic Logic: A polymodal logic that associate modalities like “know” and “suppose” with enumerated agents or groups of agents. Agents are to be interpreted in labeled transition systems by equivalence “indistinguishability” relations. A so-called Propositional Logic of Knowledge of n agents (PLKn) is sample epistemic logic.
Labeled Transition Systems or Kripke Model: An oriented labeled graph (infinite maybe). Nodes of the graph are called states or worlds, some of them are marked by propositional symbols that are interpreted to be valid in these nodes. Edges of the graph are marked by relational symbols that are interpreted by these edges.
Model Checking Problem: An algorithmic problem to validate or refute a property (presented by a formula) in a state of a model (from a class of Kripke structures). For example, model checking problem for combined logic of knowledge, actions and time in initial states of perfect recall finitely generated environments.
Perfect Recall Synchronous System: A multiagent system where every agent always records his/her observation at all moments of time while system runs.
Environment: A labeled transition system that provides an interpretation for logic of knowledge, actions and time simultaneously.
Logic of Time or Temporal Logic: A polymodal logic with a number of modalities that correspond to “next time”, “always”, “sometimes”, and “until” to be interpreted in labeled transition systems over discrete partial orders. For example, Linear Temporal Logic (LTL) is interpreted over linear orders.
MultiAgent System: A collection of communicating and collaborating agents, where every agent have some knowledge, intensions, enabilities, and possible actions.