Automated temporal equilibrium analysis: verification and synthesis of multi-player games
From MaRDI portal
Abstract: In the context of multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied. Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations. In this paper, we present such a technique. This technique relies on a reduction of the rational verification problem to the solution of a collection of parity games. Our approach has been implemented in the Equilibrium Verification Environment (EVE) system. The EVE system takes as input a model of a concurrent/multi-agent system represented using the Simple Reactive Modules Language (SRML), where agent goals are represented as Linear Temporal Logic (LTL) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an LTL formula. EVE can then check whether the LTL claim holds on some (or every) computation of the system that could arise through agents choosing Nash equilibrium strategies; it can also check whether a system has a Nash equilibrium, and synthesise individual strategies for players in the multi-player game. After presenting our basic framework, we describe our new technique and prove its correctness. We then describe our implementation in the EVE system, and present experimental results which show that EVE performs favourably in comparison to other existing tools that support rational verification.
Recommendations
- From model checking to equilibrium checking: reactive modules for rational verification
- A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
- Rational synthesis
- Automatic verification of concurrent stochastic systems
- Verification of multi-agent systems with public actions against strategy logic
Cites work
- scientific article; zbMATH DE number 42752 (Why is no real title available?)
- scientific article; zbMATH DE number 1142326 (Why is no real title available?)
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- scientific article; zbMATH DE number 7136658 (Why is no real title available?)
- scientific article; zbMATH DE number 2206109 (Why is no real title available?)
- scientific article; zbMATH DE number 2209335 (Why is no real title available?)
- A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
- A calculus of communicating systems
- A course in game theory.
- Algebraic laws for nondeterminism and concurrency
- Alternating-time temporal logic
- Augmenting ATL with strategy contexts
- Automata theory and model checking
- Basics on tree automata
- Beyond nash equilibrium
- Branching time and abstraction in bisimulation semantics
- Coordination logic
- Deciding parity games in quasipolynomial time
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Expressiveness and complexity results for strategic reasoning
- Extensive games as process models
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- From model checking to equilibrium checking: reactive modules for rational verification
- Imperfect information in reactive modules games
- Infinite games on finitely coloured graphs with applications to automata on infinite trees
- Iterated Boolean games
- Multiagent Systems
- Nash equilibrium and bisimulation invariance
- Practical verification of multi-agent systems against \textsc{Slk} specifications
- Pure Nash equilibria in concurrent deterministic games
- Quantified epistemic logics for reasoning about knowledge in multi-agent systems
- Rational synthesis
- Reasoning about coalitional games
- Reasoning about equilibria in game-like concurrent systems
- Reasoning about strategies: on the model-checking problem
- Solving parity games in practice
- Strategy logic
- Synthesis with rational environments
- The complementation problem for Büchi automata with applications to temporal logic
- The complexity of Nash equilibria in stochastic multiplayer games
- Three logics for branching bisimulation
Cited in
(16)- On the complexity of rational verification
- Characterization, verification and generation of strategies in games with resource constraints
- A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
- Stability and strategic time-dependent behaviour in multiagent systems
- Formal verification and synthesis of mechanisms for social choice
- Automatic verification of concurrent stochastic systems
- Quantitative reachability Stackelberg-Pareto synthesis is \textsf{NEXPTIME}-complete
- Incentive Engineering for Concurrent Games
- Concurrent stochastic lossy channel games
- As soon as possible but rationally
- From model checking to equilibrium checking: reactive modules for rational verification
- Stackelberg-Pareto synthesis
- Automating approximation analysis for Nash equilibria algorithms in two-player games
- Verification of multi-agent systems with public actions against strategy logic
- Automated verification of state sequence invariants in general game playing
- Automata-Based Computation of Temporal Equilibrium Models
Describes a project that uses
Uses Software
This page was built for publication: Automated temporal equilibrium analysis: verification and synthesis of multi-player games
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2211871)
