Coordination and joint ability are important problems in representation and reasoning about multi-agent systems. Ghaderi et al. presented a formalization of joint ability of coalitions in the expressive first-order language of the situation calculus. Essentially, a coalition has joint ability to achieve a goal if after iterated elimination of dominated strategies, any remaining joint strategy achieves the goal. Based on their work, Liu et al. proposed JAADL, a modal logic for joint abilities under strategy commitments. In this paper, we propose EJAADL, an epistemic extension of JAADL, for imperfect information games where agents may have incomplete knowledge or even false beliefs about the world. Like Ghaderi et al.’s work, elimination of dominated strategies is now based on beliefs about the world, rather than facts about the world as in JAADL. Strategies are required to be uniform, i.e., they select the same action in all accessible histories. We illustrate EJAADL with examples, analyze its properties, and show that model checking memoryless EJAADL is in EXPTIME. Moreover, we consider the fragment of EJAADL without the iterated elimination operator, and show that model-checking the memoryless version of this fragment can be done in PSPACE.

Representation and reasoning about strategic abilities has been an active research area in AI and multi-agent systems. Many variations and extensions of alternating-time temporal logic ATL have been proposed. However, most of the logical frameworks ignore the issue of coordination within a coalition, and are unable to specify the internal structure of strategies. In this paper, we propose JAADL, a modal logic for joint abilities under strategy commitments, which is an extension of ATL. Firstly, we introduce an operator of elimination of (strictly) dominated strategies, with which we can represent joint abilities of coalitions. Secondly, our logic is based on linear dynamic logic (LDL), an extension of linear temporal logic (LTL), so that we can use regular expressions to represent commitments to structured strategies. We analyze valid formulas in JAADL, give sufficient/necessary conditions for joint abilities, and show that model checking memoryless JAADL is in EXPTIME.