Alternating-time temporal logic with explicit strategies

We introduce ATLES – a variant of ATL with explicit names for strategies in the object language. ATLES makes it possible to refer to the same strategy in different occurrences of path quantifiers, and, as a consequence, it possible to express in ATLES some properties that cannot be expressed even in ATL∗ . We present a complete axiomatic system for ATLES. Moreover, we show that satisfiability problem for ATLES is no more complex than for ATL: it is EXPTIME-complete. We identify two variants of the model-checking problem for ATLES and investigate their computational complexity. Finally, we show how ATLES can be used to reason about extensive games.

• Type: Conference
• Year: 2007
• Where: TARK
• Authors: Dirk Walther, Wiebe van der Hoek, Michael Wooldridge
• Keywords: Explicit Names, Object Language, Path Quantifiers, TARK 2007