Iterated Boolean Games for Rational Verification
Abstract
Rational verification is the problem of understanding what temporal
logic properties hold of a multi-agent system when agents are
modelled as players in a game, each acting rationally in pursuit of
personal preferences. More specifically, rational verification asks
whether a given property, expressed as a temporal logic formula,
is satisfied in a computation of the system that might be generated
if agents within the system choose strategies for selecting actions
that form a Nash equilibrium. We show that, when agents are modelled
using the Simple Reactive Modules Language, a widely-used
system modelling language for concurrent and multi-agent systems,
this problem can be reduced to a simpler query: whether some
iterated game -- in which players have control over a finite set of
Boolean variables and goals expressed as Linear Temporal Logic
(LTL) formulae -- has a Nash equilibrium. To better understand the
complexity of solving this kind of verification problem in practice,
we then study the two-player case for various types of LTL goals,
present some experimental results, and describe a general technique
to implement rational verification using MCMAS, a model checking
tool for the verification of concurrent and multi-agent systems.