Multi-Player Games with LDL Goals over Finite Traces

TL;DR

This paper explores automata-theoretic methods for characterizing and verifying Nash equilibria in multi-player games where players have goals expressed as LDLf properties over finite traces, extending Boolean game models.

Contribution

It introduces automata-based techniques for analyzing equilibria in multi-agent systems with LDLf goals, demonstrating the regularity of Nash equilibria sets and providing complexity results.

Findings

Nash equilibria form a regular set in these games

Automata-theoretic methods effectively characterize equilibria

Complexity bounds for automata constructions are established

Abstract

Linear Dynamic Logic on finite traces LDLf is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDLf. This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because LDLf goals are considered, in the settings we study -- Reactive Modules games and iterated Boolean games with goals over finite traces -- players' goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in multi-player games with LDLf objectives is regular, and provides complexity results for the associated automata constructions.