权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Logical Foundations of Resource

资源的逻辑基础

基本信息

批准号：
EP/J002224/2
负责人：
James Brotherston
金额：
$ 53.95万
依托单位：
University College London
依托单位国家：
英国
项目类别：
Fellowship
财政年份：
2012
资助国家：
英国
起止时间：
2012 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FJ002224%2F2
关键词：
Logical Foundations Resource

项目摘要

*Resource problems* are pervasive in computer science and the real world; indeed, the fundamental concept of computation is inextricably linked with the concept of resource (time, memory, etc.). Logic provides a powerful andconvenient method for expressing and reasoning about properties of resource, and various resource-oriented logics have been advanced for this purpose in the past. Arguably the most successful application of logic-based resourcereasoning to date is the use of *separation logic* and its relatives, based on *bunched logic*, to verify memory-manipulating and concurrent computer programs. The techniques employed are, however, highly specialised to the many domain-specific properties of the verification problem; thus they do not straightforwardly transfer to other domains.While the aforementioned advances are significant, we propose that resource-oriented logics can be used to stage a much more wide-ranging and coherent attack on resource problems in general, in line with the central role of resource in a very broad spectrum of application domains. This will be achieved by providing unifying, foundational resource concepts and using these concepts to develop novel applications.Our plan is to take resource reasoning in two main new directions. The first direction is to take a much more general view of resources themselves. For example, one can consider resources which *dualise* (e.g. assets andliabilities in a financial portfolio) or which can be assembled in several different ways (much like LEGO construction bricks). The second direction is to consider not just verification but a variety of other practical resourceproblems, including resource allocation, scheduling, abduction and planning. These correspond to the way that resource problems arise in a number of fields, but have until now been little addressed by resource logics.We propose that, using suitable resource logics to express resource properties, all of the resource problems above can in fact be recast essentially as *proof search* problems. Such an approach has the potential to significantly unify these diverse resource problems, and open the way for symbolic approaches to them, which could lead to more scalable solutions (as in, e.g., symbolic model checking). Solving these proof search problems will then require search algorithms of considerable sophistication, since the search space may be far too large to explore exhaustively. We plan to employtechniques from automated theorem proving, and from reinforcement learning as used in agent-oriented computing. By combining these techniques with our symbolic methods based upon resource logics, we aim to develop formal methodsthat are both powerful and widely transferable.If this proposal achieves its research aims then we expect a significant impact on the way that resource allocation, planning and other related resource problems are handled. These problems are fundamental not only tocomputer science and its various subfields (e.g. distributed systems, agent-oriented computing, and artificial intelligence) but also to other fields such as economics, engineering, environmental science and finance, andto UK industries such as software, electronics, utility provision, transportation and manufacturing.

* 资源问题 * 在计算机科学和真实的世界中无处不在;事实上，计算的基本概念与资源（时间，内存等）的概念密不可分。逻辑为资源属性的表示和推理提供了一种强大而方便的方法，为此，人们提出了各种面向资源的逻辑。可以说，迄今为止基于逻辑的资源推理最成功的应用是使用 * 分离逻辑 * 和它的亲戚，基于 * 集束逻辑 *，来验证内存操作和并发计算机程序。所采用的技术，然而，高度专业化的许多领域的具体属性的验证问题;因此，它们不会直接转移到其他领域。虽然上述进展是重要的，但我们建议，面向资源的逻辑可以用于对一般资源问题进行更广泛和一致的攻击，这与资源在非常广泛的应用领域中的中心作用相一致。这将通过提供统一的、基础的资源概念并使用这些概念开发新的应用程序来实现。第一个方向是对资源本身采取一种更普遍的看法。例如，我们可以考虑双重化的资源（例如金融投资组合中的资产和负债），或者可以以几种不同的方式组合的资源（很像乐高积木）。第二个方向是不仅要考虑验证，还要考虑各种其他实际的资源问题，包括资源分配、调度、绑架和规划。这些对应的方式，资源问题出现在一些领域，但到目前为止，很少被解决的资源logics.We建议，使用合适的资源逻辑来表达资源属性，所有的资源问题，上述实际上可以重铸基本上是 * 证明搜索 * 的问题。这种方法有可能显著统一这些不同的资源问题，并为符号方法开辟道路，这可能导致更具可扩展性的解决方案（例如，符号模型检查）。解决这些证明搜索问题将需要相当复杂的搜索算法，因为搜索空间可能太大而无法彻底探索。我们计划采用自动定理证明技术，以及面向代理计算中使用的强化学习技术。通过将这些技术与我们基于资源逻辑的符号方法相结合，我们的目标是开发功能强大且可广泛移植的形式化方法，如果这一建议实现了其研究目标，那么我们预计将对资源分配、规划和其他相关资源问题的处理方式产生重大影响。这些问题不仅对计算机科学及其各个子领域（如分布式系统、面向代理的计算和人工智能）至关重要，而且对其他领域（如经济学、工程学、环境科学和金融）以及英国的软件、电子、公用事业、运输和制造等行业也至关重要。