Action and Knowledge in Alternating-Time Temporal Logic |
| |
Authors: | Thomas Ågotnes |
| |
Institution: | (1) Department of Informatics, University of Bergen, PB. 7800, N-5020 Bergen, Norway |
| |
Abstract: | Alternating-time temporal logic (ATL) is a branching time temporal logic in which statements about what coalitions of agents
can achieve by strategic cooperation can be expressed. Alternating-time temporal epistemic logic (ATEL) extends ATL by adding knowledge modalities, with the usual possible worlds interpretation. This paper investigates
how properties of agents’ actions can be expressed in ATL in general, and how properties of the interaction between action and knowledge can be expressed in
ATEL in particular. One commonly discussed property is that an agent should know about all available actions, i.e., that the
same actions should be available in indiscernible states. Van der Hoek and Wooldridge suggest a syntactic expression of this
semantic property. This paper shows that this correspondence in fact does not hold. Furthermore, it is shown that the semantic
property is not expressible in ATEL at all. In order to be able to express common and interesting properties of action in
general and of the interaction between action and knowledge in particular, a generalization of the coalition modalities of
ATL is proposed. The resulting logics, ATL-A and ATEL-A, have increased expressiveness without loosing ATL’s and ATEL’s tractability
of model checking. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|