Abstract:
Alternating-Time Epistemic Logic (ATEL) has been proposed recently for specification and verification of multi-agent systems properties in situations of incomplete information. Some minor problems with ATEL semantics are characterized in this paper: an agent can 'access' the current state of the whole system when making up his strategy (even when he should be uncertain about the state); moreover, no explicit representation of actions in ATEL models makes some natural situations harder to model. A few small changes are suggested in consequence, mostly to make ATEL models consistent with the incomplete information assumption.

Keywords: multiagent systems, temporal logics, transition systems, games with incomplete information.

Beware: the solutions proposed in this paper turned out not to be final and completely satisfying. Several new problems and research questions concerning ATEL semantics have been identified since the publication of the paper. In this version, some technical mistakes are corrected; however, the more fundamental issues are still left untouched. A new paper that tackles both old and newly identified problems is under preparation now.

Computational Intelligence Group @ Technical University of Clausthal
Human Media Interaction Group @ University of Twente
Computer Science Group @ University of Gdansk	Last modified 2003-08-11