Algorithm for Decision Procedure in Temporal Logic Treating Uncertainty, Plausibility, Knowledge and Interacting Agents

Algorithm for Decision Procedure in Temporal Logic Treating Uncertainty, Plausibility, Knowledge and Interacting Agents

V. Rybakov (Manchester Metropolitan University, UK)
DOI: 10.4018/978-1-4666-0158-1.ch003
OnDemand PDF Download:
$30.00
List Price: $37.50

Abstract

Our paper studies a logic UIALTL, which is a combination of the linear temporal logic LTL, a multi-agent logic with operation for passing knowledge via agents’ interaction, and a suggested logic based on operation of logical uncertainty. The logical operations of UIALTL also include (together with operations from LTL) operations of strong and weak until, agents’ knowledge operations, operation of knowledge via interaction, operation of logical uncertainty, the operations for environmental and global knowledge. UIALTL is defined as a set of all formulas valid at all Kripke-Hintikka like models NC. Any frame NC represents possible unbounded (in time) computation with multi-processors (parallel computational units) and agents’ channels for connections between computational units. The main aim of our paper is to determine possible ways for computation logical laws of UIALTL. Principal problems we are dealing with are decidability and the satisfiability problems for UIALTL. We find an algorithm which recognizes theorems of UIALTL (so we show that UIALTL is decidable) and solves satisfiability problem for UIALTL. As an instrument we use reduction of formulas to rules in the reduced normal form and a technique to contract models NC to special non-UIALTL-models, and, then, verification of validity these rules in models of bounded size. The paper uses standard results from non-classical logics based on Kripke-Hintikka models.
Chapter Preview
Top

Introduction, Initial Discussion, Aims

Temporal, modal and multi-agents’ logics motivated in AI and CS are popular areas nowadays. They are intended to describe reasoning about knowledge, properties of computational processes and basic formal laws inherent to the domain areas. Various formalizations of uncertainty in logical framework are reasonably well considered in recent publications (Crestani & Lalmas, 2001; Elvang-Goransson, Krausel, & Fox, 2006; Kaelbling, Cassandra, & Kurien, 1996; Lang, 2000; Mundici, 2000; van Rijsbergen, 2000) attempts to undertake formalizations in logical framework for plausibility are also known (Babenyshev & Rybakov, 2008). Multi-agent logics are especially broadly represented in contemporary research in AI and CS (Bordini, Fisher, Visser, & Woolridge, 2004; Dix, Fisher, Levesque, & Sterling, 2004; Fisher, 2005; Hendler, 2001; Kacprzak, 2003; van der Hoek & Woolridge, 2003). Traditionally, multi-agent system is a system composed of multiple interacting intelligent agents (though sometimes agents are considered as autonomous); multi-agent systems can be used to solve problems which are difficult or impossible for an individual agent or monolithic system to solve. Examples of problems which are appropriate to multi-agent systems research include online trading, disaster response, and modelling social structures.

Often multi-agent logics use technique from multi-modal logics (Fagin, Halpern, Moses, & Vardi, 1995; Fagin, Geanakoplos, Halpern, & Vardi, 1999; Halpern & Shore, 2004), applying modal-like operations Ki responsible for knowledge of individual agents. Any operation Ki usually behaves as S5-modality, and, therefore, technique based on Kripke multi-models may be broadly used. The exact nature of the agents is a matter of some controversy. They are sometimes claimed to be autonomous, though, in fact, autonomy is seldom desired; instead interdependent systems are needed. In particular, therefore, we intend to consider agents which may interact and pass knowledge to each other.

Another related area in logical research from AI and CS is temporal logics. One of important applications such logics in CS is specification formalism for reactive systems. Temporal logics were suggested for distinguishing properties of programs in late 1970s (Pnueli, 1977; Pnueli & Kesten, 2002). The temporal framework most used is linear-time propositional temporal logic LTL, which has been studied from various viewpoints of its application (Clark, Grumberg, & Hamaguchi, 1994; Manna & Pnueli, 1992, 1995). Temporal logic has numerous applications to safety, liveness and fairness, to various problems arising in computing (Barringer, Fisher, Gabbay & Gough, 1999). Model checking for LTL formed a direction in logic in computer science, which uses, in particular, applications of automata theory (Vardi, 1994, 1998). Temporal logics themselves can be considered as a special case of hybrid logics, e.g., as a bimodal logic with some laws imposed on interaction of modalities to imitate the flow of time. Mathematical theory devoted to study of various aspects of interaction for temporal operations (e.g., axiomatizations of temporal logics) and to construction of effective semantic theory based on Kripke/Hintikka-like models and temporal Boolean algebras, formed a highly technical branch in non-classical logics (Gabbay & Hodkinson, 1990; Goldblatt, 1992, 2003; Hodkinson, 2000; van Benthem 1983, 1991; van Benthem & Bergstra, 1994). Computational and relative problems in non-classical logics themselves formed a highly technical branch in contemporary research (Maksimova, 2003, 2006).

Complete Chapter List

Search this Book:
Reset