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, therefore, it is commonly believed that model checking of ATL(*) subsumes module checking of CTL(*). A more careful look at the known complexity results, however, makes one realize that the relationship is somewhat suspicious: module checking of CTL is Exptime-complete, while model checking of ATL is only Ptime-complete. This suggests that the relationship may not be as simple as believed. In this work, 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.

Authors

• Aniello Murano University of Naples Federico II

Keywords

No keywords are indexed for this paper.