Affiliations: Parlevink Group, University of Twente, PO Box 217,
NL-7500 AE, Enschede, Netherlands | Department of Computer Science, University of
Liverpool, Liverpool L69 7ZF, United Kingdom
Abstract: We look at ways to enrich Alternating-time Temporal Logic (ATL) – a
logic for specification and verification of multi-agent systems – with a
notion of knowledge. Starting point of our study is a recent proposal for a
system called Alternating-time Temporal Epistemic Logic (ATEL). We show that,
assuming that agents act under uncertainty in some states of the system, the
notion of allowable strategy should be defined with some caution. Moreover, we
demonstrate a subtle difference between an agent knowing that he has a suitable
strategy and knowing the strategy itself. We also point out that the agents
should be assumed similar epistemic capabilities in the semantics of both
strategic and epistemic operators. Trying to implement these ideas, we propose
two different modifications of ATEL. The first one, dubbed Alternating-time
Temporal Observational Logic (ATOL), is a logic for agents with bounded recall
of the past. With the second, ATEL-R*, we present a framework to reason about
both perfect and imperfect recall, in which we also incorporate operators for
reasoning about the past. We identify some feasible subsystems of this
expressive system.
Keywords: multiagent systems, temporal logic, epistemic logic, knowledge, transition systems, games with incomplete information
