Logical Foundations of 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.