A tool for the automated verification of Nash equilibria in concurrent games
Reactive Modules is a high-level specification language for concurrent and multi-agent systems, used in a number of practical model checking tools. Reactive Modules Games is a game-theoretic extension of Reactive Modules, in which concurrent agents in the system are assumed to act strategically in a...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer International Publishing
2015
|
| _version_ | 1797088197192187904 |
|---|---|
| author | Toumi, A Gutierrez, J Wooldridge, M |
| author_facet | Toumi, A Gutierrez, J Wooldridge, M |
| author_sort | Toumi, A |
| collection | OXFORD |
| description | Reactive Modules is a high-level specification language for concurrent and multi-agent systems, used in a number of practical model checking tools. Reactive Modules Games is a game-theoretic extension of Reactive Modules, in which concurrent agents in the system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. The basic analytical concept for Reactive Modules Games is Nash equilibrium. In this paper, we describe a tool through which we can automatically verify Nash equilibrium strategies for Reactive Modules Games. Our tool takes as input a system, specified in the Reactive Modules language, a representation of players’ goals (expressed as CTL formulae), and a representation of players strategies; it then checks whether these strategies form a Nash equilibrium of the Reactive Modules Game passed as input. The tool makes extensive use of conventional temporal logic satisfiability and model checking techniques. We first give an overview of the theory underpinning the tool, briefly describe its structure and implementation, and conclude by presenting a worked example analysed using the tool. |
| first_indexed | 2024-03-07T02:46:32Z |
| format | Conference item |
| id | oxford-uuid:ac3d7dc9-bc61-4644-a016-8ad32a4ebbca |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T02:46:32Z |
| publishDate | 2015 |
| publisher | Springer International Publishing |
| record_format | dspace |
| spelling | oxford-uuid:ac3d7dc9-bc61-4644-a016-8ad32a4ebbca2022-03-27T03:27:32ZA tool for the automated verification of Nash equilibria in concurrent gamesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:ac3d7dc9-bc61-4644-a016-8ad32a4ebbcaEnglishSymplectic Elements at OxfordSpringer International Publishing2015Toumi, AGutierrez, JWooldridge, MReactive Modules is a high-level specification language for concurrent and multi-agent systems, used in a number of practical model checking tools. Reactive Modules Games is a game-theoretic extension of Reactive Modules, in which concurrent agents in the system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. The basic analytical concept for Reactive Modules Games is Nash equilibrium. In this paper, we describe a tool through which we can automatically verify Nash equilibrium strategies for Reactive Modules Games. Our tool takes as input a system, specified in the Reactive Modules language, a representation of players’ goals (expressed as CTL formulae), and a representation of players strategies; it then checks whether these strategies form a Nash equilibrium of the Reactive Modules Game passed as input. The tool makes extensive use of conventional temporal logic satisfiability and model checking techniques. We first give an overview of the theory underpinning the tool, briefly describe its structure and implementation, and conclude by presenting a worked example analysed using the tool. |
| spellingShingle | Toumi, A Gutierrez, J Wooldridge, M A tool for the automated verification of Nash equilibria in concurrent games |
| title | A tool for the automated verification of Nash equilibria in concurrent games |
| title_full | A tool for the automated verification of Nash equilibria in concurrent games |
| title_fullStr | A tool for the automated verification of Nash equilibria in concurrent games |
| title_full_unstemmed | A tool for the automated verification of Nash equilibria in concurrent games |
| title_short | A tool for the automated verification of Nash equilibria in concurrent games |
| title_sort | tool for the automated verification of nash equilibria in concurrent games |
| work_keys_str_mv | AT toumia atoolfortheautomatedverificationofnashequilibriainconcurrentgames AT gutierrezj atoolfortheautomatedverificationofnashequilibriainconcurrentgames AT wooldridgem atoolfortheautomatedverificationofnashequilibriainconcurrentgames AT toumia toolfortheautomatedverificationofnashequilibriainconcurrentgames AT gutierrezj toolfortheautomatedverificationofnashequilibriainconcurrentgames AT wooldridgem toolfortheautomatedverificationofnashequilibriainconcurrentgames |