Combining Qualitative and Quantitative Reasoning for Logic-based Games

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 non-classical, multiple-valued 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 logically-specified games, and has the potential to greatly enrich the class of systems for which logic-based automated analysis techniques can be applied.

Although the direct applications of our research are downstream, we
can nevertheless identify several possible beneficiaries, as follows.

* First, our results will benefit that part of the computing R&D
community who must design and build systems and protocols relating
to systems in which participants act in their self-interest. This
is, we believe a large community. For example, the designers of
online trading software must take economic considerations into
account when they design their software; the designers of social
media software and group decision-making software also need to take
into account the preferences and self-interested behaviour of
participants.

* Second, our results will benefit the growing international
community interested in multi-agent systems generally, and in the
automated analysis and verification of such systems in particular,
who will gain a better understanding of the logical analysis of game
theoretic systems.

* Third, we expect our results to benefit the wider logic
community: our work will further extend the range of frameworks that
are amenable to logical analysis, and provide results that others
can build on, and algorithms that can be refined and extended.

As noted above, our project will deliver new formal models,
formalisms, and algorithms directed at the automated analysis of
distributed systems containing participants acting in pursuit of
personal goals. The concrete benefits we expect of our project include:

* understanding of the applicability of logic in general, and
Lukasiewicz logic in particular, for the specification of game theoretic
settings and protocols;

* understanding of the kinds of domains for which logic-based game
theoretic analysis is feasible and valuable;

* the capability to capture using logic complex game theoretic
scenarios, far beyond what is currently possible; and

* the capability to automatically analyse game theoretic scenarios
and protocols
using a logical (Lukasiewicz) specification.