Verification of resource-bounded multi-agent systems (VRBMAS)

A multi-agent system is a system which is comprised of multiple interacting agents. An agent is an autonomous entity that has the ability to collect information, reason about it, and perform actions based on it in pursuit of its own goals or on behalf of others. Examples of agents are controllers for automatic devices such as satellites, health care systems, non-driver transport systems such as UAVs, and even nodes in sensor networks.
Multi-agent systems are ubiquitous. Many distributed software and hardware systems can be naturally modelled as multi-agent systems. Such systems are by nature of their components extremely complex, and the interaction between components can lead to undesired behaviours that are not easy to detect. Hence, automated verification of multi-agent systems is a very important and thriving research area. We propose an important advance in this area, namely producing verification tools which allow users to specify which resources the agents need for their actions. Current tools do not offer a systematic framework for modelling resource requirements for agents' actions. However, such an ability is very important for specification of many systems, for example sensor networks where the nodes have very limited resources, e.g. energy.

A number of software and hardware incidents have made validation and verification required activities in nearly all software and hardware development processes. As a result, over the last decade, interest in tools and techniques for verification has grown exponentially, and validation and verification activities now play a central role in all stages of the development of complex and critical systems.

In addition to academic beneficiaries working in the closely related fields of verification of multi-agent systems and theoretical computer science, we expect our research to have an impact in the medium term on other academic communities. In particular, we expect our results to be beneficial in the engineering of critical and resource bounded systems, and in the analysis of protocols and processes in areas outside computer science (e.g., in engineering), thus contributing to knowledge, both with scientific advances and with novel techniques.

As a result of our project, we expect a medium/long term impact on people who will benefit from more reliable systems and on the economy by means of more efficient procedures. In the long term we expect to benefit society, by providing tools and techniques to build dependable systems that can also take into account resources.