An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking

Journal of Applied Non-Classical Logics 21 (1):93-131 (2011)
  Copy   BIBTEX

Abstract

We present a variant of ATL with incomplete information which includes the distributed knowledge operators corresponding to synchronous action and perfect recall. The cooperation modalities assume the use the distributed knowledge of coalitions and accordingly refer to perfect recall incomplete information strategies. We propose a model-checking algorithm for the logic. It is based on techniques for games with imperfect information and partially observable objectives, and involves deciding emptiness for automata on infinite trees. We also propose an axiomatic system and prove its completeness for a rather expressive subset. As for the constructs left outside this completely axiomatised subset, we present axioms by which they can be defined in the subset on the class of models in which every state has finitely many successors and give a complete axiomatisation for a “flat” subset of the logic with these constructs included.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

A quick axiomatisation of LTL with past.Martin Lange - 2005 - Mathematical Logic Quarterly 51 (1):83-88.
Axiomatisation and decidability off andp in cyclical time.Mark Reynolds - 1994 - Journal of Philosophical Logic 23 (2):197 - 224.
Memory and perfect recall in extensive games.Giacomo Bonanno - 2004 - Games and Economic Behavior 47 (2):237-256.
A logic of strategic ability under bounded memory.Thomas Ågotnes & Dirk Walther - 2009 - Journal of Logic, Language and Information 18 (1):55-77.

Analytics

Added to PP
2013-12-15

Downloads
50 (#282,682)

6 months
5 (#247,092)

Historical graph of downloads
How can I increase my downloads?