On the complexity of rational verification

DOI10.1007/S10472-022-09804-3MaRDI QIDQ6133701FDO

Authors Julian Gutiérrez, Muhammad Najib, Giuseppe Perelli, M. J. Wooldridge

Publication date 21 August 2023

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2207.02637

zbMATH Keywords

game theorymulti-agent systemstemporal logicrational verification

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Abstract: 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.

Cites work

• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• A course in game theory.
• Alternating-time temporal logic
• Automated temporal equilibrium analysis: verification and synthesis of multi-player games
• Bisection is optimal
• Deciding parity games in quasipolynomial time
• Deterministic generators and games for LTL fragments
• Expressiveness and complexity results for strategic reasoning
• Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning
• From model checking to equilibrium checking: reactive modules for rational verification
• Imperfect information in reactive modules games
• Iterated Boolean games
• Rational synthesis
• Rational synthesis under imperfect information
• Reasoning about equilibria in game-like concurrent systems
• Synthesis of Reactive(1) designs
• Synthesis with rational environments
• Temporal specifications with accumulative values
• The Complexity of Nash Equilibria in Limit-Average Games
• The complexity of mean payoff games on graphs
• The complexity of rational synthesis
• The complexity of rational synthesis for concurrent games

Cited in

(2)

• Efficient rational proofs with strong utility-gap guarantees
• scientific article; zbMATH DE number 3269880 (Why is no real title available?)

This page was built for publication: On the complexity of rational verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6133701)