Receive a 20% Discount on All Purchases Directly Through IGI Global's Online Bookstore

Nikolay V. Shilov (Russian Academy of Science, Institute of Informatics Systems, Russia) and Natalia Garanina (Russian Academy of Science, Institute of Informatics Systems, Russia)

DOI: 10.4018/978-1-59904-849-9.ch160

Chapter Preview

TopAll **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

*•**([r]*φ*)*is a formula which is read as “box*r-*φ” or “after*r*always φ*”*;*•**(*〈*r*〉φ*)*is a formula which is read as “diamond*r-*φ” or “after*r*sometimes φ*”*.

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.

Search this Book:

Reset

Copyright © 1988-2018, IGI Global - All Rights Reserved