Iterated games with LDL goals
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: | , , |
|---|---|
| Format: | Conference item |
| Published: |
Association for Computing Machinery
2017
|
| _version_ | 1826307031373447168 |
|---|---|
| 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 setting we study— iterated Boolean games with goals over finite traces (iBGF )—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 (Nash) equilibria, shows that the set of Nash equilibria in games with LDL F objectives is regular, and provides complexity results for the associated automata constructions. |
| first_indexed | 2024-03-07T06:56:54Z |
| format | Conference item |
| id | oxford-uuid:fe70e3ef-8be4-4c2e-8c7c-206a4f13edae |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:56:54Z |
| publishDate | 2017 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:fe70e3ef-8be4-4c2e-8c7c-206a4f13edae2022-03-27T13:36:28ZIterated games with LDL goalsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:fe70e3ef-8be4-4c2e-8c7c-206a4f13edaeSymplectic Elements at OxfordAssociation for Computing Machinery2017Gutierrez, 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 setting we study— iterated Boolean games with goals over finite traces (iBGF )—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 (Nash) equilibria, shows that the set of Nash equilibria in games with LDL F objectives is regular, and provides complexity results for the associated automata constructions. |
| spellingShingle | Gutierrez, J Perelli, G Wooldridge, M Iterated games with LDL goals |
| title | Iterated games with LDL goals |
| title_full | Iterated games with LDL goals |
| title_fullStr | Iterated games with LDL goals |
| title_full_unstemmed | Iterated games with LDL goals |
| title_short | Iterated games with LDL goals |
| title_sort | iterated games with ldl goals |
| work_keys_str_mv | AT gutierrezj iteratedgameswithldlgoals AT perellig iteratedgameswithldlgoals AT wooldridgem iteratedgameswithldlgoals |