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.

Multi-player games with LDL goals over finite traces / Gutierrez, J.; Perelli, G.; Wooldridge, M.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 276:(2021). [10.1016/j.ic.2020.104555]

Multi-player games with LDL goals over finite traces

Perelli G.;
2021

Abstract

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.
2021
Formal verification; Games; Multi-agent systems; Temporal logic
01 Pubblicazione su rivista::01a Articolo in rivista
Multi-player games with LDL goals over finite traces / Gutierrez, J.; Perelli, G.; Wooldridge, M.. - In: INFORMATION AND COMPUTATION. - ISSN 0890-5401. - 276:(2021). [10.1016/j.ic.2020.104555]
File allegati a questo prodotto
File Dimensione Formato  
Gutierrez_preprint_Multi-player_2020.pdf

accesso aperto

Note: https://doi.org/10.1016/j.ic.2020.104555
Tipologia: Documento in Pre-print (manoscritto inviato all'editore, precedente alla peer review)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 319.39 kB
Formato Adobe PDF
319.39 kB Adobe PDF
Gutierrez_Multi-player_2021.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 518.3 kB
Formato Adobe PDF
518.3 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/1403477
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact