Iterated Games with LDL Goals over Finite Traces
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 setting we study -- iterated Boolean games with
goals over finite traces (iBGF) -- 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 (Nash) equilibria, shows that the set of Nash equilibria
in games with LDLF objectives is regular, and provides complexity
results for the associated automata constructions.