On Module Checking and Strategies

Two decision problems are very close in spirit: module checking of CTL/CTL* and model checking of ATL/ATL*. The latter appears to be a natural multi-agent extension of the former, and it is commonly believed that model checking of ATL(*) subsumes module checking of CTL(*) in a straightforward way. Perhaps because of that, the exact relationship between the two has never been formally established. A more careful look at the known complexity results, however, makes one realize that the relationship is somewhat suspicious. In particular, module checking of CTL is EXPTIME-complete, while model checking of ATL is only P-complete. Thus, the (seemingly) less expressive framework yields significantly higher computational complexity than the (seemingly) more expressive one. This suggests that the relationship may not be as simple as believed. In this paper, we show that the difference is indeed fundamental. The way in which behavior of the environment is understood in module checking cannot be equivalently characterized in ATL(*). Conversely, if one wants to embed module checking in ATL(*) then its semantics must be extended with two essential features, namely nondeterministic strategies and long-term commitment to strategies.