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

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 K_i responsible for knowledge of individual agents. Any operation K_i 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).