Logical Foundations of Resource
Lead Research Organisation:
Queen Mary University of London
Department Name: Sch of Electronic Eng & Computer Science
Abstract
*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 and
convenient 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 resource
reasoning 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 and
liabilities 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 resource
problems, 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 employ
techniques 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 methods
that 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 to
computer 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, and
to UK industries such as software, electronics, utility provision, transportation and manufacturing.
convenient 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 resource
reasoning 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 and
liabilities 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 resource
problems, 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 employ
techniques 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 methods
that 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 to
computer 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, and
to UK industries such as software, electronics, utility provision, transportation and manufacturing.
Planned Impact
In this proposal we aim to develop the logical foundations of *resource-oriented logics*, and to apply these logics in a variety of novel ways to resource problems that occur in computer science and in the wider public domain, such as the efficient allocation of resources. To take a concrete example of such a problem, suppose a TV channel is selling advertising slots during its World Cup coverage (say). Advertisers submit bids offering a certain amount of money
for slots of a certain duration occurring during certain commercial breaks. Furthermore, an advertiser might require multiple slots (to maximise impact or because their advert has more than one part) so that a set of slots is valued higher than the sum of its parts. The problem for the TV channel is, given a number of bids from advertisers, how to allocate their limited airtime to bids in such a way as to maximise their revenue. This is a typical *combinatorial auction* problem that arises over and over again in many different situations. Our research has the potential to open the way for symbolic approaches to this problem, which could ultimately lead to more scalable solutions (as in, e.g., symbolic model checking). We also hope to significantly unify a number of diverse resource problems - e.g. verification, allocation, scheduling, plan synthesis, abduction - that are found not only throughout computer science but also in other fields such as economics, engineering, environmental science and finance, and in major industries such as software, electronics, utility provision, transportation and manufacturing. Such problems typically have significant implications for the efficient use of resources and therefore ultimately the cost of "doing business"'. Consequently, the use of resource logics to develop scalable and robust solutions to these problems has the long-term potential for substantial impact in several fields and areas of the economy.
We explicitly identify two (mainly disjoint) groups of entities on (mainly disjoint) critical pathways to the aforementioned economic and societal impacts:
Group I: researchers and organisations *within* computer science with a *commercial* interest in computer-aided resource reasoning applications such as verification and distributed systems. They will benefit from the new insights and reasoning techniques provided by our research programme, which could form the basis of new commerical computerised tools for solving resource problems. Indeed, we will collaborate directly with our project partners Parkinson (Microsoft Research) and Calcagno (Monoidics) on providing prototype tool support for our methods.
Group II: researchers and organisations *mainly outside* computer science (e.g. economists or financial analysts) with an *academic and/or commercial* interest in resource problems such as resource allocation and scheduling, e.g., the information security firm Sapphire and the logistics IT firm CombineNet. Such organisations even potentially include governmental departments. They will benefit from our introduction of logical methods to resource problems of practical industrial interest (such as large-scale combinatorial auctions) which could lead to more efficient and scalable solutions to these problems. One of our Project Partners, Prof. David Pym at the University of Aberdeen, falls within this group through his participation in two TSB-funded grants: "Cloud Stewardship Economics" and "Trust Economics", held with several industrial partners including HP Labs. Both projects involve information security and system-scale modelling. By collaborating with Pym we hope to take advantage of opportunities for technology transfer from our theoretical work to the wider industrial setting.
for slots of a certain duration occurring during certain commercial breaks. Furthermore, an advertiser might require multiple slots (to maximise impact or because their advert has more than one part) so that a set of slots is valued higher than the sum of its parts. The problem for the TV channel is, given a number of bids from advertisers, how to allocate their limited airtime to bids in such a way as to maximise their revenue. This is a typical *combinatorial auction* problem that arises over and over again in many different situations. Our research has the potential to open the way for symbolic approaches to this problem, which could ultimately lead to more scalable solutions (as in, e.g., symbolic model checking). We also hope to significantly unify a number of diverse resource problems - e.g. verification, allocation, scheduling, plan synthesis, abduction - that are found not only throughout computer science but also in other fields such as economics, engineering, environmental science and finance, and in major industries such as software, electronics, utility provision, transportation and manufacturing. Such problems typically have significant implications for the efficient use of resources and therefore ultimately the cost of "doing business"'. Consequently, the use of resource logics to develop scalable and robust solutions to these problems has the long-term potential for substantial impact in several fields and areas of the economy.
We explicitly identify two (mainly disjoint) groups of entities on (mainly disjoint) critical pathways to the aforementioned economic and societal impacts:
Group I: researchers and organisations *within* computer science with a *commercial* interest in computer-aided resource reasoning applications such as verification and distributed systems. They will benefit from the new insights and reasoning techniques provided by our research programme, which could form the basis of new commerical computerised tools for solving resource problems. Indeed, we will collaborate directly with our project partners Parkinson (Microsoft Research) and Calcagno (Monoidics) on providing prototype tool support for our methods.
Group II: researchers and organisations *mainly outside* computer science (e.g. economists or financial analysts) with an *academic and/or commercial* interest in resource problems such as resource allocation and scheduling, e.g., the information security firm Sapphire and the logistics IT firm CombineNet. Such organisations even potentially include governmental departments. They will benefit from our introduction of logical methods to resource problems of practical industrial interest (such as large-scale combinatorial auctions) which could lead to more efficient and scalable solutions to these problems. One of our Project Partners, Prof. David Pym at the University of Aberdeen, falls within this group through his participation in two TSB-funded grants: "Cloud Stewardship Economics" and "Trust Economics", held with several industrial partners including HP Labs. Both projects involve information security and system-scale modelling. By collaborating with Pym we hope to take advantage of opportunities for technology transfer from our theoretical work to the wider industrial setting.
People |
ORCID iD |
| James Brotherston (Principal Investigator / Fellow) |