Game-Theoretic Semantics for Alternating-Time Temporal Logic

DOI10.1145/3179998MaRDI QIDQ4691736zbMATH OpenOpenAlexWikidataFDO

Authors Antti Kuusisto, Raine Rönnholm, Valentin Goranko

Publication date 24 October 2018

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1602.07667, http://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-161056

zbMATH Keywords

argumentation-based dialogue and protocolslogic and game theorylogics for agents and multiagent systems

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in artificial intelligence (68T27) Agent technology and artificial intelligence (68T42) Applications of game theory (91A80)

Abstract: We introduce versions of game-theoretic semantics (GTS) for Alternating-Time Temporal Logic (ATL). In GTS, truth is defined in terms of existence of a winning strategy in a semantic evaluation game, and thus the game-theoretic perspective appears in the framework of ATL on two semantic levels: on the object level in the standard semantics of the strategic operators, and on the meta-level where game-theoretic logical semantics is applied to ATL. We unify these two perspectives into semantic evaluation games specially designed for ATL. The game-theoretic perspective enables us to identify new variants of the semantics of ATL based on limiting the time resources available to the verifier and falsifier in the semantic evaluation game. We introduce and analyse an unbounded and (ordinal) bounded GTS and prove these to be equivalent to the standard (Tarski-style) compositional semantics. We show that in these both versions of GTS, truth of ATL formulae can always be determined in finite time, i.e., without constructing infinite paths. We also introduce a non-equivalent finitely bounded semantics and argue that it is natural from both logical and game-theoretic perspectives.

Recommendations

• Temporal logics for games
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Games for Temporal Logics on Trees
• Satisfiability games for branching-time logics
• Alternative semantics for temporal logics
• Alternating-time temporal logic with finite-memory strategies
• Complete axiomatization and decidability of alternating-time temporal logic
• Alternating-time temporal logic
• Timed Alternating-Time Temporal Logic
• Temporal logic with preferences and reasoning about games

Cited in

(7)

• Bounded game-theoretic semantics for modal mu-calculus
• Game-theoretic semantics for \(\mathrm{ATL}^+\) with applications to model checking
• Alternating-time temporal logic ATL with finitely bounded semantics
• Embedding Alternating-time Temporal Logic in Strategic Logic of Agency
• Model-Checking Timed ATL for Durational Concurrent Game Structures
• Bounded game-theoretic semantics for modal mu-calculus and some variants
• A formal framework for reasoning about agents' independence in self-organizing multi-agent systems

This page was built for publication: Game-Theoretic Semantics for Alternating-Time Temporal Logic

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