Game-theoretic semantics for \(\mathrm{ATL}^+\) with applications to model checking

DOI10.1016/j.ic.2020.104554zbMath1497.68303arXiv1702.08405OpenAlexW3013111319MaRDI QIDQ2225595

Raine Rönnholm, Antti Kuusisto, Valentin F. 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

zbMATH Keywords

game-theoretic semanticsalternating-time temporal logicalgorithmic model checkingfinite memory strategiestractable fragments

Mathematics Subject Classification ID

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

Related Items (4)

The optimal way to play the most difficult repeated two-player coordination games ⋮ Unnamed Item ⋮ Strategic reasoning with a bounded number of resources: the quest for tractability ⋮ Bounded game-theoretic semantics for modal mu-calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Alternating-time temporal logic ATL with finitely bounded semantics
• Automata and fixed point logic: a coalgebraic perspective
• Finitary winning in ω-regular games
• Verifying agents with memory is harder than it seemed
• Alternating-time temporal logic
• On the Expressiveness and Complexity of ATL
• ATL with Strategy Contexts and Bounded Memory
• EXPTIME Tableaux for the Coalgebraic μ-Calculus
• Game-Theoretic Semantics for Alternating-Time Temporal Logic
• Positional Determinacy of Games with Infinitely Many Priorities
• From Liveness to Promptness

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