Logical Foundations of Resource

Lead Research Organisation: University College London
Department Name: 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.

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.

Publications

10 25 50

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/J002224/1 01/12/2011 01/06/2012 £465,503
EP/J002224/2 Transfer EP/J002224/1 02/06/2012 01/12/2016 £423,410
 
Description This project, an EPSRC Career Acceleration Fellowship, aimed to investigate resource problems from a logical perspective.

Much of the research focused on exploring the logical foundations of "separation logic", which it has evolved from a novel way of reasoning about pointers in computer memory to a mainstream technique for scalable verification of software (used e.g. at Facebook) in order to understand what we can and cannot hope to do automatically, and how the technology might be pushed beyond its initial limitations. The project established a number of fundamental theoretical results about the tractability of problems in this area, both positive and negative.

One of the key technologies developed in this area was that of *cyclic proof*, an alternative way of doing proofs by induction based on circular proof graphs. Cyclic proof offers a significant advantage for automatic proof search, as employed in program verification and in mechanical theorem provers, by delaying difficult choices during a proof until exploration of the proof search space makes suitable choices more evident. We developed the first ever first ever fully-automatic, general-purpose cyclic theorem prover (CYCLIST) and showed it to be highly competitive with the state of the art. In fact, it is now the default approach for theorem proving in separation logic where one has user-defined data structures in the memory.

More generally, we also looked at "bunched logics", which can be used to describe general properties of *resource*. Bunched logic provides the foundation for separation logic, where "resource" is interpreted as heap memory in a suitably chosen model. However, there is a whole spectrum of interesting such logics, some of which offer new ways of potentially reasoning about computer memory, and others which offer ways of reasoning about quite different types of resource. We investigated a number of such logics and showed that they might be used for reasoning about more sophisticated types of resource than had previously been accounted for.
Exploitation Route Much of the work is already being widely cited and built on by academics working on automated verification and logic. High-tech companies such as Facebook and Amazon Web Services are also incorporating verification into their software development chains, and Facebook in particular has displayed an interest in pursuing future collaborations based on our previous work in this area.
Sectors Digital/Communication/Information Technologies (including Software)

 
Description Facebook Faculty Grant 2015
Amount $30,000 (USD)
Organisation Facebook 
Sector Private
Country United States
Start 10/2015 
End 09/2018
 
Description Nikos 
Organisation Middlesex University
Country United Kingdom 
Sector Academic/University 
PI Contribution Ongoing academic research collaboration
Collaborator Contribution Ongoing academic research collaboration
Impact CSL-LICS 2014 paper "A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates" SAS'14 paper "Cyclic Abduction of Inductively Defined Safety and Termination Preconditions" Cyclist theorem prover
Start Year 2013
 
Description Raj 
Organisation Australian National University (ANU)
Country Australia 
Sector Academic/University 
PI Contribution Joint work on research project into Craig interpolation for displayable logics
Collaborator Contribution Joint work on research project into Craig interpolation for displayable logics
Impact TABLEAUX 2011 publication: Craig Interpolation for Displayable Logics by Brotherston and Gore. IJCAR 2016 publication: Machine-checked interpolation theorems for substructural logics using display calculi by Dawson, Brotherston and Gore
Start Year 2010
 
Title Cyclist 2014 
Description Updated the Cyclist theorem prover with substantial new techniques and features, as described in related publications. 
Type Of Technology Software 
Year Produced 2014 
Open Source License? Yes  
Impact Cyclist was entered into and performed well in the new SL-COMP competition for separation logic theorem provers. 
URL https://github.com/ngorogiannis/cyclist
 
Title SL disprover 
Description Given an entailment A |= B between two formulas in separation logic with inductive predicates, this tool attempts to disprove the entailment, i.e. to infer the existence of a countermodel. 
Type Of Technology Software 
Year Produced 2014 
Open Source License? Yes  
Impact First disprover for separation logic. Opens up potential new applications in speeding up verification and automatic proof search, and in automated theory exploration. 
URL https://github.com/ngorogiannis/cyclist
 
Title SL model checker 
Description Compares the heap memory of a running program against an assertion written in separation logic with general inductive definitions. 
Type Of Technology Software 
Year Produced 2015 
Open Source License? Yes  
Impact First model checker of its kind, with potential applications to verification and software testing. 
URL https://github.com/ngorogiannis/cyclist