Abstract

We investigate a series of logics that allow to reason about agents' actions, abilities, and their knowledge about actions and abilities. These logics include Pauly's Coalition Logic CL, Alternating-time Temporal Logic ATL, the logic of ‘seeing-to-it-that' (STIT), and epistemic extensions thereof. While complete axiomatizations of CL and ATL exist, only the fragment of the STIT language without temporal operators and without groups has been axiomatized by Xu (called Ldm). We start by recalling a simplification of the Ldm that has been proposed in previous work, together with an alternative semantics in terms of standard Kripke models. We extend that semantics to groups via a principle of superadditivity, and give a sound and complete axiomatization that we call Ldm G. We then add a temporal ‘next' operator to Ldm G, and again give a sound and complete axiomatization. We show that Ldm G subsumes coalition logic CL. Finally, we extend these logics with standard S5 knowledge operators. This enables us to express that agents see to something under uncertainty about the present state or uncertainty about which action is being taken. We focus on the epistemic extension of X-Ldm G, noted E-X-Ldm G. In accordance with established terminology in the planning community, we call this extension of X-Ldm G the conformant X-Ldm G. The conformant X-Ldm G enables us to express that agents are able to perform a uniform strategy. We conclude that in that respect, our epistemic extension of X-Ldm G is better suited than epistemic extensions of ATL.