Game-theoretic semantics for ATL^+ with applications to model checking

DOI10.1016/J.IC.2020.104554MaRDI QIDQ2225595zbMATH OpenOpenAlexFDO

Authors Antti Kuusisto, Raine Rönnholm, Valentin Goranko

Publication date 8 February 2021

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

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

zbMATH Keywords

algorithmic model checkingalternating-time temporal logicfinite memory strategiesgame-theoretic semanticstractable fragments

Mathematics Subject Classification ID

Temporal logic (03B44) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: We develop game-theoretic semantics (GTS) for the fragment ATL+ of the full Alternating-time Temporal Logic ATL*, essentially extending a recently introduced GTS for ATL. We first show that the new game-theoretic semantics is equivalent to the standard semantics of ATL+ (based on perfect recall strategies). We then provide an analysis, based on the new semantics, of the memory and time resources needed for model checking ATL+. Based on that, we establish that strategies that use only a very limited amount of memory suffice for ATL+. Furthermore, using the GTS we provide a new algorithm for model checking of ATL+ and identify a natural hierarchy of tractable fragments of ATL+ that extend ATL.

Recommendations

• Game-Theoretic Semantics for Alternating-Time Temporal Logic
• Alternating-time temporal logic with finite-memory strategies
• Alternating-time temporal logic
• ATL with Strategy Contexts and Bounded Memory
• Model-Checking Timed ATL for Durational Concurrent Game Structures

Cites work

• Alternating-time temporal logic
• Alternating-time temporal logic ATL with finitely bounded semantics
• Alternating-time temporal logic with finite-memory strategies
• ATL with Strategy Contexts and Bounded Memory
• Automata and fixed point logic: a coalgebraic perspective
• CTL with finitely bounded semantics
• EXPTIME Tableaux for the Coalgebraic μ-Calculus
• Finitary winning in \({\omega}\)-regular games
• From Liveness to Promptness
• Game-Theoretic Semantics for Alternating-Time Temporal Logic
• scientific article; zbMATH DE number 3399180 (Why is no real title available?)
• scientific article; zbMATH DE number 3190338 (Why is no real title available?)
• On the Expressiveness and Complexity of ATL
• Positional Determinacy of Games with Infinitely Many Priorities
• Verifying agents with memory is harder than it seemed

Cited in

(9)

• Bounded game-theoretic semantics for modal mu-calculus
• Strategic reasoning with a bounded number of resources: the quest for tractability
• Model-checking games for typed -calculi
• Concurrent game structures with roles
• Model-Checking Timed ATL for Durational Concurrent Game Structures
• Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)
• Alternating-time temporal logic with finite-memory strategies
• Bounded game-theoretic semantics for modal mu-calculus and some variants
• The optimal way to play the most difficult repeated two-player coordination games

This page was built for publication: Game-theoretic semantics for \(\mathrm{ATL}^+\) with applications to model checking

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