From Model Checking to Equilibrium Checking: Reactive Modules for Rational Verification
Abstract
Model checking is the best-known and most successful approach to formally verifying
that systems satisfy specifications, expressed as temporal logic formulae.
In this article, we develop the theory of equilibrium checking, a related but distinct
problem. Equilibrium checking is relevant for multi-agent systems in which
system components (agents) are assumed to be acting rationally in pursuit of delegated
goals, and is concerned with understanding what temporal properties hold
of such systems under the assumption that agents select strategies in equilibrium.
The formal framework we use to study this problem assumes agents are modelled
using REACTIVE MODULES, a system modelling language that is used in a
range of practical model checking systems. Each agent (or player) in a REACTIVE
MODULES game is specified as a nondeterministic guarded command program,
and each player's goal is specified with a temporal logic formula that the player
desires to see satisfied. A strategy for a player in a REACTIVE MODULES game
defines how that player selects enabled guarded commands for execution over
successive rounds of the game. For this general setting, we investigate games in
which players have goals specified in Linear Temporal Logic (in which case it
is assumed that players choose deterministic strategies) and in Computation Tree
Logic (in which case players select nondeterministic strategies). For each of these
cases, after formally defining the game setting, we characterise the complexity of
a range of problems relating to Nash equilibria (e.g., the computation or the verification
of existence of a Nash equilibrium or checking whether a given temporal
formula is satisfied on some Nash equilibrium). We then go on to show how the
model we present can be used to encode, for example, games in which the choices
available to players are specified using STRIPS planning operators.