Multi-player games with LDL goals over finite traces

DOI10.1016/J.IC.2020.104555MaRDI QIDQ2225596zbMATH OpenOpenAlexFDO

Authors Julian Gutiérrez, Giuseppe Perelli, M. J. Wooldridge

Publication date 8 February 2021

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2008.05647

zbMATH Keywords

multi-agent systemstemporal logicgamesformal verification

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60) Agent technology and artificial intelligence (68T42) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Reasoning about equilibria in game-like concurrent systems
• Expressiveness and complexity results for strategic reasoning
• Logics for Reasoning About Strategic Abilities in Multi-player Games
• Equilibria for games with combined qualitative and quantitative objectives
• Iterated Boolean games

Cites work

• scientific article; zbMATH DE number 1136080 (Why is no real title available?)
• scientific article; zbMATH DE number 1444727 (Why is no real title available?)
• scientific article; zbMATH DE number 7297884 (Why is no real title available?)
• A course in game theory.
• Emptiness Of Alternating Tree Automata Using Games With Imperfect Information
• Expressiveness and complexity results for strategic reasoning
• From model checking to equilibrium checking: reactive modules for rational verification
• Iterated Boolean games
• Logics for Reasoning About Strategic Abilities in Multi-player Games
• Model checking a path (preliminary report)
• Rational synthesis
• Reasoning about strategies: on the model-checking problem
• Strategy logic
• Synthesis with rational environments
• The complementation problem for Büchi automata with applications to temporal logic
• The complexity of propositional linear temporal logics
• The stuttering principle revisited
• Uniform strategies, rational relations and jumping automata

Cited in

(1)

• First-order temporal logic on finite traces: semantic properties, decidable fragments, and applications

Describes a project that uses

Uses Software

• MOCHA

This page was built for publication: Multi-player games with LDL goals over finite traces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225596)