Automated temporal equilibrium analysis: Verification and synthesis of multi-player games
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 ar...
| Main Authors: | , , , |
|---|---|
| 格式: | Journal article |
| 语言: | English |
| 出版: |
Elsevier
2020
|
| _version_ | 1826293542997196800 |
|---|---|
| author | Gutierrez, J Najib, M Perelli, G Wooldridge, M |
| author_facet | Gutierrez, J Najib, M Perelli, G Wooldridge, M |
| author_sort | Gutierrez, J |
| collection | OXFORD |
| description | 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 (Image 1) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an Image 1 formula. EVE can then check whether the Image 1 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. |
| first_indexed | 2024-03-07T03:31:44Z |
| format | Journal article |
| id | oxford-uuid:baf504e4-aabd-4939-bbe3-2023d7fe75c6 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T03:31:44Z |
| publishDate | 2020 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:baf504e4-aabd-4939-bbe3-2023d7fe75c62022-03-27T05:13:26ZAutomated temporal equilibrium analysis: Verification and synthesis of multi-player gamesJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:baf504e4-aabd-4939-bbe3-2023d7fe75c6EnglishSymplectic ElementsElsevier2020Gutierrez, JNajib, MPerelli, GWooldridge, MIn 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 (Image 1) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an Image 1 formula. EVE can then check whether the Image 1 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. |
| spellingShingle | Gutierrez, J Najib, M Perelli, G Wooldridge, M Automated temporal equilibrium analysis: Verification and synthesis of multi-player games |
| title | Automated temporal equilibrium analysis: Verification and synthesis of multi-player games |
| title_full | Automated temporal equilibrium analysis: Verification and synthesis of multi-player games |
| title_fullStr | Automated temporal equilibrium analysis: Verification and synthesis of multi-player games |
| title_full_unstemmed | Automated temporal equilibrium analysis: Verification and synthesis of multi-player games |
| title_short | Automated temporal equilibrium analysis: Verification and synthesis of multi-player games |
| title_sort | automated temporal equilibrium analysis verification and synthesis of multi player games |
| work_keys_str_mv | AT gutierrezj automatedtemporalequilibriumanalysisverificationandsynthesisofmultiplayergames AT najibm automatedtemporalequilibriumanalysisverificationandsynthesisofmultiplayergames AT perellig automatedtemporalequilibriumanalysisverificationandsynthesisofmultiplayergames AT wooldridgem automatedtemporalequilibriumanalysisverificationandsynthesisofmultiplayergames |