Multi-player games with LDL goals over finite traces
Linear Dynamic Logic on finite traces (LDLF) is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using...
| Main Authors: | , , |
|---|---|
| 格式: | Journal article |
| 语言: | English |
| 出版: |
Elsevier
2019
|
| _version_ | 1826296152121671680 |
|---|---|
| author | Gutierrez, J Perelli, G Wooldridge, M |
| author_facet | Gutierrez, J Perelli, G Wooldridge, M |
| author_sort | Gutierrez, J |
| collection | OXFORD |
| description | Linear Dynamic Logic on finite traces (LDLF) is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on (LDLF). This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because (LDLF) goals are considered, in the settings we study—Reactive Modules games and iterated Boolean games with goals over finite traces—players' goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in multi-player games with (LDLF) objectives is regular, and provides complexity results for the associated automata constructions. |
| first_indexed | 2024-03-07T04:11:56Z |
| format | Journal article |
| id | oxford-uuid:c81d9161-c3dd-4c70-8e7f-c38d4ed9deb5 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T04:11:56Z |
| publishDate | 2019 |
| publisher | Elsevier |
| record_format | dspace |
| spelling | oxford-uuid:c81d9161-c3dd-4c70-8e7f-c38d4ed9deb52022-03-27T06:49:58ZMulti-player games with LDL goals over finite tracesJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:c81d9161-c3dd-4c70-8e7f-c38d4ed9deb5EnglishSymplectic Elements at OxfordElsevier2019Gutierrez, JPerelli, GWooldridge, MLinear Dynamic Logic on finite traces (LDLF) is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on (LDLF). This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because (LDLF) goals are considered, in the settings we study—Reactive Modules games and iterated Boolean games with goals over finite traces—players' goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in multi-player games with (LDLF) objectives is regular, and provides complexity results for the associated automata constructions. |
| spellingShingle | Gutierrez, J Perelli, G Wooldridge, M Multi-player games with LDL goals over finite traces |
| title | Multi-player games with LDL goals over finite traces |
| title_full | Multi-player games with LDL goals over finite traces |
| title_fullStr | Multi-player games with LDL goals over finite traces |
| title_full_unstemmed | Multi-player games with LDL goals over finite traces |
| title_short | Multi-player games with LDL goals over finite traces |
| title_sort | multi player games with ldl goals over finite traces |
| work_keys_str_mv | AT gutierrezj multiplayergameswithldlgoalsoverfinitetraces AT perellig multiplayergameswithldlgoalsoverfinitetraces AT wooldridgem multiplayergameswithldlgoalsoverfinitetraces |