Verifying requirements for resource-bounded agents
Lead Research Organisation:
University of Nottingham
Department Name: School of Computer Science
Abstract
The project will provide theoretical foundations and practical tools foranalysing resource requirements for systems of reasoning agents, suchas, for example, agents which reason using ontological rules to providea web service. The resources we shall consider include the time,memory, and communication bandwidth required by the agents to select thenext action to perform.The trend towards ever smaller agent platforms means that resourceutilisation is becoming an increasingly important factor in agent design and deployment.However the complex, often distributed, derivations implied by modernagent designs make it hard for agent developers to predict system resourcerequirements a priori. The development of formal frameworks andpractical verification tools to exploit them is therefore key to thesuccessful development of provably correct agent designs for emergingresource-limited agent paradigms such as mobile agents and platformssuch as PDAs and smart phones.The project builds on the previous joint work between the investigators andvisiting researchers using model-checking techniques to verify requirements.
Organisations
Publications
Albore Alexandre
(2009)
Bounded-Resource Reasoning as (Strong or Classical) Planning
in Proceedings of the 9th International Workshop Computational Logic in Multi-Agent Systems (CLIMA IX), Revised Selected and Invited Papers, Springer LNCS
Alechina N
(2009)
Belief ascription under bounded resources
in Synthese
Alechina N
(2009)
Verifying time, memory and communication bounds in systems of reasoning agents
in Synthese
Alechina N.
(2010)
Logic for coalitions with bounded resources
in Journal of Logic and Computation
Alechina Natasha
(2008)
A Logic of Situated Resource-Bounded Agents
in Journal of Logic, Language and Information
Nguyen H
(2018)
Alternating-time temporal logic with resource bounds
in Journal of Logic and Computation
| Description | The project developed theoretical foundations and practical tools for analysing resource requirements for systems of reasoning agents, such as, for example, a system of communicating rule-based agents or agents which reason using resolution. The resources we considered with respect to reasoning agents were time, memory, and communication bandwidth required by the agents to achieve a goal (e.g., select an action). We developed logics which explicitly referred to resources, enabling us to precisely formulate properties of such systems with respect to resource requirements. We proved soundness, completeness and decidability results for those logics, and demonstrated examples of key resource trade-offs. For example, when solving a distributed reasoning problem, we can demonstrate the extent to which time can be traded for memory or for the number of exchanged messages. In addition, we have developed a verification framework based on the Maude model checker that can verify resource requirements of systems of resource-bounded rule-based reasoners. As an extension of the original aims of the project, we generalised logics for modelling resource-bounded reasoners in two directions. First, we moved from describing actions of single reasoners to talking about abilities of groups of agents, building on existing logics such as Coalition Logic and Alternating-Time Temporal Logic. This enabled us to describe strategies of groups of agents, for example, that a particular group of agents has a strategy to achieve a given goal within a specified resource bound. Being able to express the abilities of groups of agents also enabled us to use abstraction -- essentially representing a group of agents as a single agent -- which is very useful for scalable modelling. Second, we generalised logics so that we could talk about arbitrary actions (not just inference steps and sending messages) and arbitrary resources (not just time, memory and number of messages). This makes the logical formalisms more flexible and transparent, and applicable to a much wider range of resource verification problems. The resulting logics, which we called RBCL for resource-bounded coalition logic and RBATL for resource-bounded alternating time temporal logic, enable us to formulate properties of resource requirements of agents in a multi-agent system and automatically verify whether those properties hold. We have established model-checking complexity results for those logics and also provided complete and sound axiomatisations. |
| Exploitation Route | The findings have generated interest in the community of researchers on verification of multi-agent systems. Several research groups are working on the algorithms for model-checking resource-bounded systems. Our group is continuing the work now funded by the EPSRC grant EP/K033905/1 the output of which is going to be a practical model-checking tool for resource-bounded systems, as well as new theoretical developments for systems with both production and consumption of resources. |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software) |
| Description | The work continues to be used only in academic setting, but the current research aims to develop a practical verification tool that can be used by practitioners in industry. This work is funded by the EPSRC grant EP/K033905/1 together with the developer of the model-checking tool MCMAS Franco Raimondi funded by EP/K033921/1. |
| First Year Of Impact | 2014 |
| Sector | Digital/Communication/Information Technologies (including Software) |