EPSRC Reference: 
EP/M009130/1 
Title: 
Combining Qualitative and Quantitative Reasoning for Logicbased Games 
Principal Investigator: 
Wooldridge, Professor M 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Oxford 
Scheme: 
Standard Research 
Starts: 
01 December 2014 
Ends: 
31 May 2018 
Value (£): 
271,272

EPSRC Research Topic Classifications: 
Artificial Intelligence 
Fundamentals of Computing 
Robotics & Autonomy 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
17 Jul 2014

EPSRC ICT Prioritisation Panel  July 2014

Announced


Summary on Grant Application Form 
The use of game theoretic techniques in computer science is becoming ever more prevalent. One reason for this is that in many of the systems we want to build, participants cannot be assumed to be benevolent: instead, they must be assumed to be rational agents, acting in pursuit of their own personal goals. For such systems, game theory provides a natural analytical framework. In our work, we are interested in the automated analysis of such systems using techniques for model checking, which over the past two decades have proved to be enormously influential. In model checking, the idea is to express desirable system properties as logical formula, and then to check whether these properties actually hold of the given system. A key problem if we want to extend existing verification techniques to game theoretic settings is that the formalisms used in model checking do not allow us to directly represent the preferences or utilities of players (i.e., their goals). This project is directed at this problem. The basic idea is that we can use a formalism known as Lukasiewicz logic to express the "utility function" for players, which represent their preferences. Lukasiewicz logic is a nonclassical, multiplevalued logic which has the attractive property that Lukasiewicz formulae can represent a very rich class of utility functions  much richer than is possible using classical logic. The project will lay the theoretical groundwork for this new and exciting class of logicallyspecified games, and has the potential to greatly enrich the class of systems for which logicbased automated analysis techniques can be applied.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.ox.ac.uk 