An executable theory of multi-agent systems refinement

Leiden Repository

An executable theory of multi-agent systems refinement

Type: Doctoral Thesis
Title: An executable theory of multi-agent systems refinement
Author: Aştefănoaei, Lăcrămioara
Publisher: Center for Mathematics and Computer Science (CWI), Faculty of Science, Leiden University
Issue Date: 2011-01-19
Keywords: Agent methodology and languages
Formal verification
Multi-agent systems
Normative rules
Refinement
Rewriting logic
(Timed) Coordination
Verification
Weakest precondition calculus
Abstract: 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.
Description: Promotores: F.S. de Boer, J.J.Ch. Meyer, Co-promotor: M. Dastani
With summary in Dutch
Faculty: Faculteit der Wiskunde en Natuurwetenschappen
Citation: Aştefănoaei, L., 2011, Doctoral thesis, Leiden University
Series/Report no.: IPA dissertation series ; 2011-4
ISBN: 9789064644504
Handle: http://hdl.handle.net/1887/16343
 

Files in this item

Description Size View
application/pdf Cover 3.327Mb View/Open
application/pdf Full text 1.008Mb View/Open
application/pdf Propositions 1.555Mb View/Open

This item appears in the following Collection(s)