Verifying requirements for resource-bounded agents

该项目将为分析推理代理系统的资源需求提供理论基础和实用工具，例如，使用本体论规则进行推理以提供网络服务的代理。我们将考虑的资源包括代理选择下一个动作执行所需的时间、内存和通信带宽。越来越小的代理平台的趋势意味着资源利用率正在成为代理设计和部署中越来越重要的因素。然而，现代代理设计所隐含的复杂的、通常是分布式的派生使得代理开发者很难预先预测系统资源需求。因此，开发正式的框架和实用的验证工具以利用它们是成功开发可证明正确的代理设计的关键，这些设计适用于新兴的资源有限的代理范例，如移动代理和PDA和智能手机等平台。该项目建立在调查人员和访问研究人员以前的联合工作的基础上，使用模型检查技术来验证需求。

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.