دورية أكاديمية

Multi-player games with LDL goals over finite traces

التفاصيل البيبلوغرافية
العنوان: Multi-player games with LDL goals over finite traces
المؤلفون: Gutierrez J., Perelli G., Wooldridge M.
المساهمون: Gutierrez, J., Perelli, G., Wooldridge, M.
بيانات النشر: Elsevier Inc.
سنة النشر: 2021
المجموعة: Sapienza Università di Roma: CINECA IRIS
مصطلحات موضوعية: Formal verification, Game, Multi-agent system, Temporal logic
الوصف: 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.
نوع الوثيقة: article in journal/newspaper
اللغة: English
العلاقة: info:eu-repo/semantics/altIdentifier/wos/WOS:000607516300006; volume:276; numberofpages:16; journal:INFORMATION AND COMPUTATION; http://hdl.handle.net/11573/1403477Test; info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-85082814589
DOI: 10.1016/j.ic.2020.104555
الإتاحة: https://doi.org/10.1016/j.ic.2020.104555Test
http://hdl.handle.net/11573/1403477Test
حقوق: info:eu-repo/semantics/openAccess
رقم الانضمام: edsbas.9D848560
قاعدة البيانات: BASE