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: 2EXPTIMEcomplete 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