Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games

TL;DR

This paper introduces a new technique for verifying properties of multi-agent systems by reducing rational verification to parity games, implemented in the EVE system, enabling strategy synthesis and equilibrium checking.

Contribution

The paper presents a novel reduction-based approach for rational verification of multi-agent systems, implemented in the EVE tool, improving efficiency and capability over existing methods.

Findings

EVE efficiently verifies equilibrium properties in multi-agent systems.

EVE can synthesize strategies for agents in multi-player games.

Experimental results show EVE outperforms existing tools.

Abstract

In the context of multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied. Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations. In this paper, we present such a technique. This technique relies on a reduction of the rational verification problem to the solution of a collection of parity games. Our approach has been implemented in the Equilibrium Verification Environment (EVE) system. The EVE system takes as input a model of a concurrent/multi-agent system represented using the Simple Reactive Modules Language (SRML), where agent goals are represented as Linear Temporal Logic (LTL) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an LTL formula. EVE can then check whether the LTL claim holds on some (or every) computation of the system that could arise through agents choosing Nash equilibrium strategies; it can also check whether a system has a Nash equilibrium, and synthesise individual strategies for players in the multi-player game. After presenting our basic framework, we describe our new technique and prove its correctness. We then describe our implementation in the EVE system, and present experimental results which show that EVE performs favourably in comparison to other existing tools that support rational verification.