Embedding Alternating-time Temporal Logic in Strategic STIT Logic of Agency

Seeing To It That (STIT) 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 [varphi]'. We believe that STIT theory can contribute to the logical analysis of multiagent systems. To su...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logic and computation 2006-10, Vol.16 (5), p.559-578
Main Authors: Broersen, Jan, Herzig, Andreas, Troquard, Nicolas
Format: Article
Language:English
Subjects:
Artificial Intelligence
Computer Science
Logic in Computer Science
Multiagent Systems
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Seeing To It That (STIT) 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 [varphi]'. We believe that STIT 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. 23-35) where we presented a translation from Pauly's Coalition Logic to Chellas' STIT logic. Here we focus on Alur, Henzinger and Kupferman's Alternating-time Temporal Logic (ATL), and the logic of the 'fused' [open diamond]s[_scstit : _] operator for strategic ability, as described by Horty. After a brief presentation of ATL and the definition of a discrete-time strategic STIT framework slightly adapted from Horty, we give a translation from ATL to the STIT framework, and prove that it determines correct embedding.
ISSN:0955-792X
1465-363X
DOI:10.1093/logcom/exl025