Rational verification refers to the problem of checking which temporal logic
properties hold of a concurrent multiagent system, under the assumption that
agents in the system choose strategies that form a game-theoretic equilibrium.
Rational verification can be understood as a counterpart to model checking for
multiagent systems, but while classical 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
harder: the key decision problems for rational verification are
2EXPTIME-complete with LTL specifications, even when using explicit-state
system representations. Against this background, our contributions in this
paper are threefold. First, 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 a broad and practically useful class of
response properties of reactive systems. In particular, we show that for a
number of relevant settings, rational verification can be done in polynomial
space and even in polynomial time. Second, we provide improved complexity
results for rational verification when considering players' goals given by
mean-payoff utility functions; arguably the most widely used approach for
quantitative objectives in concurrent and multiagent systems. Finally, we
consider the problem of computing outcomes that satisfy social welfare
constraints. To this end, we consider both utilitarian and egalitarian social
welfare and show that computing such outcomes is either PSPACE-complete or
NP-complete.

本文讨论了针对具有博弈均衡策略的并发多智能体系统进行时间逻辑性质检查的合理性验证问题，并提出了减少验证复杂度的有效方法。同时研究了满足社会福利约束条件的多智能体系统的最优策略问题。