Logic-Based Agent Verification
The multi-agent paradigm has become increasingly prevalent in computer science. Such popularity is due to its ability to capture social, economic, and other relevant interactions within a task. To meet the increasing demand for multi-agent systems, substantial progress has been made in theoretical, experimental and practical development.
Most recently, concerns have been raised regarding the trustworthiness of such systems. This issue is especially pertinent to military, aerospace, and commercial applications, but it also plays a role in numerous other applications. Recent swarm systems, with hundreds to thousands of agents, have increased the level of concern. The problem, in particular, is one of addressing the question of whether a collection of agents, while collaborating to satisfy a common goal, can be trusted to not only satisfy that goal but also satisfy additional safety-critical constraints. These constraints might arise from physical agent distances, required agent interactions with people, speed-of-response requirements, safety considerations in a manufacturing environment, or the need to ensure the security of classified information.
To address these issues, a small but growing community has evolved to study the problem in a formal context. Early work was presented at a series of workshops on Formal Approaches to Agent-Based Systems (FAABS) [5-7], as well as in the AAMAS conferences and relevant journals [2,3]. As an outgrowth of this early research, work on this topic has evolved into three main subtopics: formal agent modeling, formal verification of multi-agent systems, and applications research. The primary formalism that dominates the work is logic-based, and therefore the work fits well with the topic of this journal.
This special issue of the Journal of Applied Logic contains six papers on state-of-the-art research on the topic of assuring the trustworthiness of multi-agent systems. The collection of papers in this issue provides good coverage of the field, in the sense that the papers jointly span all three subtopics mentioned above and they are quite representative of the current state of the field.
The first three papers focus primarily on agent interaction protocols, and they address both the specification and verification of multi-agent systems. The paper entitled "Verifiable agent dialogues", by Walton, develops a new multiagent system (MAS) protocol language for multi-agent dialogues that is based on process calculus. This specification language is applicable to a wide range of agent architectures. In the latter half of the paper, a transformation is presented that enables the formal specifications to be translated into another language expressly designed for efficient and effective formal verification, based on model checking. Model checking consists of building a finite model of a (multi-agent) system and checking whether a desired property holds in that model [1]. In logic notation, model checking determines whether S |= P for model S and property P . In Walton's paper, properties are expressed in linear temporal logic, and the MAS is based on the Belief-Desire-Intention (BDI) framework [4].
Giordano, Martelli, and Schwind's paper, "Specifying and verifying interaction protocols in a temporal action logic", has similar objectives to those of the Walton paper. In particular, they aim to specify and verify multi-agent interaction protocols. Verification is again based on model checking. although in this case it can be formalized as either a validity or a satisfiability problem. Giordano et al. present a logical specification framework that is based on dynamic linear-time temporal logic (DLTL), which is an extension of LTL. Following Singh [8], Giordano et al. adopt a social approach to agent communication. In this approach, communicative actions affect the "social state" of the