Multi-player games with LDL goals over finite traces

DOI10.1016/J.IC.2020.104555zbMATH Open1497.68305arXiv2008.05647OpenAlexW3013665479MaRDI QIDQ2225596FDOQ2225596

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

Publication date: 8 February 2021

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

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.

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The complexity of propositional linear temporal logics
• Reasoning About Strategies
• Synthesis with rational environments
• Rational Synthesis
• Iterated Boolean games
• Strategy logic
• The complementation problem for Büchi automata with applications to temporal logic
• CONCUR 2003 - Concurrency Theory
• The stuttering principle revisited
• From model checking to equilibrium checking: reactive modules for rational verification
• Emptiness Of Alternating Tree Automata Using Games With Imperfect Information
• Logics for Reasoning About Strategic Abilities in Multi-player Games
• Uniform strategies, rational relations and jumping automata

Cited In (1)

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

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)