Designing Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2023
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866913614905999360 |
|---|---|
| author | Gutierrez, Julian Najib, Muhammad Perelli, Giuseppe Wooldridge, Michael |
| author_facet | Gutierrez, Julian Najib, Muhammad Perelli, Giuseppe Wooldridge, Michael |
| contents | In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we explore the concept of equilibrium design, where incentives are designed to obtain a desirable equilibrium that satisfies a specific temporal logic property. Our study is based on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players' goals as mean-payoff objectives. We consider system specifications given by LTL and GR(1) formulae, and show that designing incentives to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game can be achieved in PSPACE for LTL properties and in NP/ΣP 2 for GR(1) specifications. We also examine the complexity of related decision and optimisation problems, such as optimality and uniqueness of solutions, as well as considering social welfare, and show that the complexities of these problems lie within the polynomial hierarchy. Equilibrium design can be used as an alternative solution to rational synthesis and verification problems for concurrent games with mean-payoff objectives when no solution exists or as a technique to repair concurrent games with undesirable Nash equilibria in an optimal way. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_03045 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Designing Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints Gutierrez, Julian Najib, Muhammad Perelli, Giuseppe Wooldridge, Michael Logic in Computer Science Computer Science and Game Theory Multiagent Systems In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we explore the concept of equilibrium design, where incentives are designed to obtain a desirable equilibrium that satisfies a specific temporal logic property. Our study is based on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players' goals as mean-payoff objectives. We consider system specifications given by LTL and GR(1) formulae, and show that designing incentives to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game can be achieved in PSPACE for LTL properties and in NP/ΣP 2 for GR(1) specifications. We also examine the complexity of related decision and optimisation problems, such as optimality and uniqueness of solutions, as well as considering social welfare, and show that the complexities of these problems lie within the polynomial hierarchy. Equilibrium design can be used as an alternative solution to rational synthesis and verification problems for concurrent games with mean-payoff objectives when no solution exists or as a technique to repair concurrent games with undesirable Nash equilibria in an optimal way. |
| title | Designing Equilibria in Concurrent Games with Social Welfare and Temporal Logic Constraints |
| topic | Logic in Computer Science Computer Science and Game Theory Multiagent Systems |
| url | https://arxiv.org/abs/2306.03045 |