Alternating-Time Temporal Announcement Logic

摘要

We propose a formalism that we call Alternating-time Temporal Announcement Logic (ATAL). It can be seen as an extension of the Coalition Announcement Logic (CAL) proposed by Agotnes et al. As well as CAL, ATAL has modal operators enabling to express sentences like 'there is an action a by group of agents G after which consequence Φ is true, in spite of what the other agents do'. One of the differences here, is that such action α can also be a physical action, and not only public announcements, as in CAL. Based on the latter kind of operator, ATAL also presents operators similar to those in Alternating-time Temporal Logic, which enable to express agents abilities. For instance, ATAL has operators enabling to express sentences like 'the group of agents G is able to enforce that Φ is true from the next step on until ψ becomes true'. We also provide a sound and complete axiomatization for ATAL and draw comparisons with several other logics, such as Public Announcement Logic with Assignment, Arbitrary Public Announcement Logic, Coalition Logic and Alternating-time Temporal Logic.