Alternating-time temporal logic with explicit strategies
Dirk Walther, Wiebe van der Hoek, Michael Wooldridge · 2007
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.