Agent interaction: abstract approaches to modelling, programming and verifying multi-agent systems

Computer systems and their applications are becoming increasingly more complicated. Modern systems often consist of multiple independent parts (hardware and software), which interact with their environment. Computers communicate with other computers, exchange information with and receive commands from their human users and receive information about their physicalor virtual environment. This high degree of interactivity leadsto an inherently larger degree of complexity, which needs to be managed and controlled. An important means to reduce complexity is abstraction. Abstraction meansfinding intuitive concepts to model the complex reality and leaving outunderlying details. In the field of multi-agent systems, in which the work ofthis thesis fits, anthropomorphic abstractions are oftenused. Anagent is an autonomous piece of software, designed and/or built in terms ofanthropomorphic concepts, which interacts with other agents and its environmentin such a way that it takes into account the dynamic circumstances and strives to achieve its aims. In this thesis, we focus on agent interaction. Starting from different viewpoints in the field ofmulti-agent systems, we introduce a number of new abstract concepts for agentinteraction. A danger of using abstraction is that abstract concepts areintroduced without grounding them in the computational reality. Therefore, wetake care to always relate our abstract notions to lower-level concepts. We start in Chapter 2 by anchoring three already existing and popular agentconcepts, which are belief, desire and intention, in externally observableagent behaviour. We provide criteria which formally describe when behaviour of an agent indicates that the agent has a certainmental state (a belief, desire or intention). These criteria can be used by agents themselves to attribute belief, desire and intention to other agents, onthe basis of observed behaviour. Chapter 3 deals with agent verification. As the complexity of agent systems ishigh, verification of these systems is very difficult. We develop two principleswhich aid in making verification of agent systems more manageable. The firstprinciple is language abstraction. We use two logical languages to phraseproperties, an abstract one and a detailed one. Properties in theabstract language are shorter and more intuitive than properties in thedetailed language. The second principle is constructing abstract, generic,reusable systems of properties and proofs. In Chapter 4 we present a new model of agents, which focuses on agentinteraction. Our model explicitly includes the dynamic environment. We have areal-time model: actions have a duration. This means that actions of one or more agents can takeplace during overlapping time frames, leading to harmful interference orbeneficial synergy. Agents can perform group actions, which means that themembers of the group perform individual actions in a coordinated manner. In Chapter 5, we develop the programming language GrAPL (Group AgentProgramming Language), intended to program multi-agent systems in which agentscan form temporary alliances to perform group actions. Before a group actions isperformed, the agents communicate with each other to pose demands on details ofthe action and the composition of the group of actors. The programming languagehas a formal operational semantics. We generalise the idea of Chapter 5 in Chapter 6, by looking at group plansinstead of group actions. A group plan is a composed action, consisting of bothindividual actions and group actions, which are partially ordered in time. Weprovide a new high-level coordination language which heterogeneous agents canuse to discuss group plans and to execute them in a synchronised manner