Abstract
We study here a variant of the alternating-time temporal logic (ATL) where each agent has a given memory. We show that it is an interesting compromise, rather realistic but with a reasonable complexity. In contrast, most models with perfect recall and imperfect information have an undecidable model-checking

Abstract
In this paper we propose a logic-based social approach to the specification and verification of agent interaction. We firstly introduce integrity constraints about social acts (called Social Integrity Constraints) as a formalism to express interaction protocols and to give a social semantics to the behavior of agents, focusing on communicative acts. Then, we discuss several possible kinds of verification of agent interaction, and we show how social integrity constraints can be used to verify some properties in this respect. We focus our attention on static verification of compliance of agent specifications to interaction protocols, and on run-time verification, based on agents' observable behavior. We adopt as a running example the NetBill security transaction protocol for the selling and delivery of information goods.

Abstract
We introduce and motivate a non-standard multi-modal logic to represent and reason about ignorance in Multi-Agent Systems. We argue that in Multi-agent systems being able to reason about what agents ignore is just as important as being able to reason about what agents know. We show a sound and complete axiomatisation for the logic. We investigate its applicability by restating the feasibility condition for the FIPA communication primitive of inform.

Abstract
A dialogue game is presented that describes coherent conversational sequences with inconsistent and biased information between agents at the speech act level. These types of information are represented with the use of a multi-valued logic based on a bilattice structure. This approach makes it possible to devise a dialogue game in which agents can deliberate their cognitive states with inconsistent and biased information.

Abstract
The ultimate goal of our research is to develop techniques for model checking knowledge properties of multi-agent systems. ATEL, an extension of the Alternating-time Temporal Logic of Alur et al, is a logic for specifying epistemic and strategic properties of such systems. We present a technique for reducing the ATEL model checking problem to one of model checking in ATL, whereby epistemic relations are explicitly encoded in ATL models as as dynamic transitions. The techniques is illustrated by means of a knowledge game, which is used as a running example throughout the paper.

Abstract
We present a compiler that translates a multi-agent systems specification given in the formalism of Interpreted Systems into an SMV program. We show how an SMV model checker can be coupled with a Kripke model editor (Akka) to allow for the mechanical verification of epistemic properties of multi-agent systems.

Abstract
The current ACL proposals show some shortcomings with respect to the definition of their semantics. Our paper aims at tackling those issues by defining an ACL semantics as a specification of the analytical effects of agent communicative acts. We analyze agent communication in terms of concepts taken from Speech Act Theory, as several researchers have already done, but move away from the mainstream view of artificial agent research, as we define communicative acts in terms of changes at the level of social relationship between agents. We take commitment to be a primitive concept underlying the social dimension of multiagent systems, and define a basic artificial institution whose aim is to provide agents with the means to affect the commitment network that binds them to each other.