Theory, Verification

Two decision problems are very close in spirit: module check-ing 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 straight-forward 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 some-what suspicious. In particular, module checking of CTL is EXPTIME-complete, while model checking of ATL is only P-complete. Thus, the (seemingly) less expressive frame-work 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 fundamen-tal. The way in which behavior of the environment is un-derstood in module checking cannot be equivalently char-acterized in ATL(*). Conversely, if one wants to embed module checking in ATL(*) then its semantics must be ex-tended with two essential features, namely nondeterministic strategies and long-term commitment to strategies