An executable Theory of Multi-Agent Systems Refinement

Complex applications such as incident management, social simulations, manufacturing applications, electronic auctions, e-institutions, and business to business applications are pervasive and important nowadays. Agent-oriented methodology is an advance in abstraction which can be used by software developers to naturally model and develop systems for such applications. In general, with respect to design methodologies, what it may be important to stress is that control structures should be added at later stages of design, in a natural top-down manner going from specifications to implementations, by refinement. Too much detail (be it for the sake of efficiency) in specifications often turns out to be harmful. To paraphrase D.E. Knuth, “Premature optimization is the root of all evil” (quoted in ‘The Unix Programming Environment’ by Kernighan and Pine, p. 91). The aim of this thesis is to adapt formal techniques to the agent-oriented methodology into an executable theory of refinement. The justification for doing so is to provide correct agent-based software by design. The underlying logical framework of the theory we propose is based on rewriting logic, thus the theory is executable in the same sense as rewriting logic is. The storyline is as follows. We first motivate and explain constituting elements of agent languages chosen to represent both abstract and concrete levels of design. We then propose a definition of refinement between agents written in such languages. This notion of refinement ensures that concrete agents are correct with respect to the abstract ones. The advantage of the definition is that it easily leads to formulating a proof technique for refinement via the classical notion of simulation. This makes it possible to effectively verify refinement by model-checking. Additionally, we propose a weakest precondition calculus as a deductive method based on assertions which allow to prove correctness of infinite state agents. We generalise the refinement relation from single agents to multi-agent systems in order to ensure that concrete multi-agent systems refine their abstractions. We see multi-agent systems as collections of coordinated agents, and we consider coordination artefacts as being based either on actions or on normative rules. We integrate these two orthogonal coordination mechanisms within the same refinement theory extended to a timed framework. Finally, we discuss implementation aspects.