Affordable Access

Alternating-time temporal logic with finite-memory strategies

Authors
Publication Date
Keywords
  • Model-Checking The Alternating-Time Temporal Logics Atl And Atl* With Incomplete Information Is Unde
  • However
  • When Restricting To Memoryless Strategies The Model-Checking Problem Becomes Decidable
  • In This Paper We Consider Two Other Types Of Semantics Based On Finite-Memory Strategies
  • One Where The Memory Size Allowed Is Bounded And One Where The Memory Size Is Unbounded (But Must Be
  • This Is Motivated By The High Complexity Of Model-Checking With Perfect Recall Semantics And The Sev
  • We Show That Both Types Of Semantics Introduced Are Different From Perfect Recall And Memoryless Sem
  • In Particular
  • We Show That The Complexity Of Model-Checking With Bounded-Memory Semantics Is Delta_2P-Complete For
  • We Also Present A Proof That Atl And Atl* Model-Checking Is Undecidable For N &Gt
  • = 3 Players With Finite-Memory Semantics In Incomplete Information Games
Disciplines
  • Linguistics

Abstract

Alternating-time temporal logic with finite-memory strategies - DTU Orbit (27/04/14) Alternating-time temporal logic with finite-memory strategies - DTU Orbit (27/04/14) Alternating-time temporal logic with finite-memory strategies Model-checking the alternating-time temporal logics ATL and ATL* with incomplete information is undecidable for perfect recall semantics. However, when restricting to memoryless strategies the model-checking problem becomes decidable. In this paper we consider two other types of semantics based on finite-memory strategies. One where the memory size allowed is bounded and one where the memory size is unbounded (but must be finite). This is motivated by the high complexity of model-checking with perfect recall semantics and the severe limitations of memoryless strategies. We show that both types of semantics introduced are different from perfect recall and memoryless semantics and next focus on the decidability and complexity of model-checking in both complete and incomplete information games for ATL/ATL*. In particular, we show that the complexity of model-checking with bounded-memory semantics is Delta_2p-complete for ATL and PSPACE-complete for ATL* in incomplete information games just as in the memoryless case. We also present a proof that ATL and ATL* model-checking is undecidable for n >= 3 players with finite-memory semantics in incomplete information games. General information State: Published Organisations: Department of Applied Mathematics and Computer Science , Algorithms and Logic Authors: Vester, S. (Intern) Pages: 194–207 Publication date: 2013 Host publication information Title: Proceedings Fourth International Symposium on Games, Automata, Logics and Formal Verification Series: Electronic Proceedings in Theoretical Computer Science Volume: 119 ISSN (print): 2075-2180 Main Research Area: Technical/natural sciences Conference: 4th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2013), Borca di Cadore, Dolomi

There are no comments yet on this publication. Be the first to share your thoughts.