Rational verification in multi-agent systems

Thesis

Rational verification problem is concerned with checking which temporal logic properties will hold in a system composed of multiple agents which are assumed to behave rationally and strategically in pursuit of individual objectives. Unfortunately, the problem is generally hard from computational point of view, and for the purpose of practical implementations, usually requires specialised techniques.

This thesis aims to develop algorithms and study computational complexity results for rational verification in multi-agent systems. Firstly, a practically amenable technique which relies on a reduction to the solution of a collection of parity games is proposed. The technique in this thesis uses a model of strategies that is bisimulation invariant—that is, in which individual strategies for system components are valid across all bisimilar systems, and which satisfy the same temporal logic properties in equilibrium. This approach has been implemented in the Equilibrium Verification Environment (EVE) system. Secondly, some cases in which the problem of rational verification is computationally tractable are investigated. In particular, it is shown that the complexity of rational verification can be reduced from 2EXPTIME-complete to fixed-parameter tractable. Furthermore, improved complexity results when considering quantitative goals, namely mean-payoff utility functions, are also studied. In doing so, a concept called equilibrium design is proposed. This concept is concerned with the design of incentives so that a desirable equilibrium is obtained.

Authors: Najib, M

• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: Model checking; Automata; Temporal logic; Games; Synthesis; Computational complexity; Nash equilibrium
• Subjects: Multi-Agent Systems; Artificial intelligence; Formal Verification; Algorithmic Game Theory