Tech Reports

ULCS-09-015

Reasoning about Time, Action and Knowledge in Multi-Agent Systems (PhD Thesis)

Ji Ruan

Abstract

This thesis provides a logic-based account for Multi-Agent Systems (MASs) specification and verification, in terms of time, action and knowledge. Chapter 1 describes the research area of MASs, the motivation for this research, and the methods chosen. Chapter 2 provides a logical background for the work: it first introduces temporal logics from a single-agent perspective (Linear-time Temporal Logic and Computational Tree Logic), and from a multi-agent perspective (Alternating-time Temporal Logic), and then goes on to introduce two types of epistemic logics that deal with knowledge and change in MASs (Temporal Epistemic Logic and Dynamic Epistemic Logic). A literature review is provided, along with the definitions of languages and semantics of these logics, and the computational complexities of these logics.

The main contributions of this thesis are presented in the next four chapters, from Chapter 3 to Chapter 6. Chapter 3 and Chapter 4 are focused on the verification of games in the Game Description Language (GDL), a declarative language used in General Game Playing Competition. The aim of the competition is to provide a platform for researchers to develop general purpose game playing systems, which shall have more flexibility compared to dedicated game playing systems such as the famous Chess-playing system Deep Blue. While GDL is specifically designed for describing games, it can also be seen as a language to describe a class of MASs. A practical problem for a designer of games or MASs using GDL is to check whether they meets desired specifications. One formalism for reasoning about games that has attracted much interest is Alternating-time Temporal Logic (ATL). Chapter 3 investigates the connection between GDL and ATL. It first demonstrates that GDL can be understood as a specification language for ATL models. Subsequently it shows that it is possible to succinctly characterise GDL game descriptions directly as ATL formulas, and that, as a corollary, the problem of interpreting ATL formulas over GDL descriptions is EXPTIME-Complete. Then in Chapter 4, this connection is explored more practically. In particular, two main contributions are made: firstly, a characterization of the playability conditions which can be used to express the correctness of the games specified in GDL, and secondly an automated tool that uses an ATL model checker to verify the playability conditions for the games described in GDL. The feasibility of our approach is demonstrated by a case study on the game called Tic-Tac-Toe.

Chapters 5 and 6 are focused on the modelling of MASs with incomplete information. In particular, a study of correspondence between Dynamic Epistemic Logic (DEL) and Temporal Epistemic Logic (TEL) is made. These two logical frameworks are capable of modelling MASs with agents' knowledge and change. However, there is an apparent difference in terms of model checking: in DEL the interpretation of a dynamic epistemic formula is over a state model, which represents a static view of a MAS; while in TEL, the interpretation of a temporal epistemic formula is over an interpreted system, in which the full history of a system is unfolded. Chapter 5 links DEL and TEL, showing that DEL can be embedded into a version of TEL. In particular, given an epistemic state and a formula in DEL, we construct an interpreted system relative to that epistemic state and that formula that satisfies the translation of that formula into TEL. The construction involves that the protocol that is implicit in the dynamic epistemic formula, i.e., the set of sequences of actions being executed to evaluate the formula, is made explicit. We first focus on the public announcement logic, a simpler version of DEL with actions being public announcements only, then generalize our results to the full version of DEL. Chapter 6 proceeds at studying model checking knowledge dynamics with three state-of-the-art model checkers for MASs. We first discuss the role of protocols in model checking processes, and proceed with case studies of two problems. With the Russian Cards Problem, we show how to use model checking tools to specify and verify communication protocols, and how dynamic epistemic modelling and temporal epistemic modelling compare in practice. With the Sum And Product Problem, we show an important feature supported by the dynamic epistemic model checker DEMO, but not by the temporal epistemic model checkers MCK and MCMAS. We also compare the model checking results of different variants of this problem, and discuss the influence of model checking time by different representations of a same specification.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.