|
|
Abstract
Model checking techniques are concerned with the formal verification of software.
Their aim is to prove in a formal and precise way that particular properties are satisfied by a certain system.
While model checking is now an established area of research in software engineering of (traditional) distributed systems,
this is not the case in multi-agent systems (MAS). MAS is a new and rapidly growing paradigm in computing for modelling
and implementing distributed systems where the entities are complex, autonomous, and interacting with one another.
Although MAS has been proven to be a successful paradigm for modelling and building critical applications,
they still lack the tools for a formal verification.
Current model checking tools abstract away from the crucial notions in use in MAS, such as knowledge,
beliefs, intentions, etc, of the components of the system, and so they cannot be readily applied to MAS verification.
This research aims at filling this gap by studying and developing tools and techniques that will enable MAS verification.
|