On Computational Tractability for Rational Verification
Abstract
Rational verification involves checking which temporal logic
properties hold of a concurrent/multiagent system, under the
assumption that agents in the system choose strategies in game
theoretic equilibrium. Rational verification can be understood as a
counterpart of model checking for multiagent systems, but while
model checking can be done in polynomial time for some temporal
logic specification languages such as CTL, and polynomial space
with LTL specifications, rational verification is much more
intractable: 2EXPTIME-complete with LTL specifications, even when
using explicit-state system representations. In this paper we show
that the complexity of rational verification can be greatly reduced
by restricting specifications to GR(1), a fragment of LTL that can
represent most response properties of reactive systems. We also
provide improved complexity results for rational verification when
considering players' goals given by mean-payoff utility
functions -- arguably the most widely used quantitative objective for
agents in concurrent and multiagent systems. In particular, we show
that for a number of relevant settings, rational verification can be
done in polynomial space or even in polynomial time.