Journal of Logic and Computation Advance Access originally published online on September 12, 2006
Journal of Logic and Computation 2006 16(5):559-578; doi:10.1093/logcom/exl025
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||
Original Articles |
Embedding Alternating-time Temporal Logic in Strategic
Logic of Agency
Department of Information and Computing Sciences, Universiteit Utrecht, Utrecht, The Netherlands.
Institut de Recherche en Informatique de Toulouse, CNRS, Université Paul Sabatier, Toulouse, France. E-mail: herzig{at}irit.fr
Institut de Recherche en Informatique de Toulouse, Université Paul Sabatier, Toulouse, France & Laboratorio di Ontologia Applicata, Università degli Studi di Trento, Trento, Italy. E-mail: troquard{at}irit.fr
E-mail: broersen{at}cs.uu.nl
Seeing To It That (
) logic is a logic of agency, proposed in the 1990s in the domain of philosophy of action. It is the logic of constructions of the form agent a sees to it that
. We believe that
theory can contribute to the logical analysis of multiagent systems. To support this claim, we show that there is a close relationship with more recent logics for multiagent systems. This work extends Broersen et al. (2006, Electron Notes Theor. Comput. Sci., Vol. 157, pp. 2335) where we presented a translation from Pauly's Coalition Logic to Chellas'
logic. Here we focus on Alur, Henzinger and Kupferman's Alternating-time Temporal Logic
, and the logic of the fused
s[_scstit : _] operator for strategic ability, as described by Horty. After a brief presentation of ATL and the definition of a discrete-time strategic
framework slightly adapted from Horty, we give a translation from ATL to the
framework, and prove that it determines correct embedding.
Keywords: Modal logic; multi-agent systems; agency; strategic choice; philosophical foundations