TY - JOUR

T1 - On the complexity of rational verification

AU - Gutierrez, Julian

AU - Najib, Muhammad

AU - Perelli, Giuseppe

AU - Wooldridge, Michael

N1 - Funding Information:
Wooldridge gratefully acknowledges the support of the ERC under Advanced Grant 291528 (“RACE”), and the support of the Alan Turing Institute in London. Najib acknowledges the support of ERC Starting Grant 759969 (AV-SMP). Perelli acknowledges the support of the ERC project “WhiteMech” (grant agreement No 834228) and the EU ICT-48 2020 project TAILOR (No. 952215).
Publisher Copyright:
© 2022, The Author(s).

PY - 2023/8

Y1 - 2023/8

N2 - 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.

AB - 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.

KW - Game theory

KW - Multi-agent systems

KW - Rational verification

KW - Temporal logic

UR - http://www.scopus.com/inward/record.url?scp=85134293064&partnerID=8YFLogxK

U2 - 10.1007/s10472-022-09804-3

DO - 10.1007/s10472-022-09804-3

M3 - Article

AN - SCOPUS:85134293064

SN - 1012-2443

VL - 91

SP - 409

EP - 430

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

ER -