Action and knowledge in alternating-time temporal logic (Q2500827)

The paper mainly deals with the expressive power of alternating-time temporal epistemic logic [cf. \textit{W. van der Hoek} and \textit{M. Wooldridge}, ``Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications,'' Stud. Log. 75, No. 1, 125--157 (2003; Zbl 1034.03013)], in particular, concerning the interplay between knowledge and actions of agents. The crucial property in question is \textit{\((*)\) complete knowledge about available actions}. This property is formalized in the relevant semantic domains, and it is shown that neither existing attempts nor any ATEL-formula at all can capture \((*)\). The formal language is then extended to the effect that the cooperation modalities are indexed not only with a set of agents but also with a set of actions. In this way, the actions by means of which the agents can achieve some goal at a certain state are made explicit. Several examples showing the expressiveness of the new language are given, and it is proved, in particular, that \((*)\) can be captured now. Finally, it is shown that model checking can be done in polynomial time for the extended system, too.