ATL and Strategy Logic (SL) are important languages for representation and reasoning about strategic abilities of coalitions in multi-agent systems. In analyzing strategies of agents in multi-agent systems, an important concept to consider is rationality. Strategy Logic can express rationality concepts such as Nash Equilibrium (NE). Recently, there has been work on logics for joint abilities incorporating rationality concepts based on iterated elimination of dominated strategies (IEDS). Each of NE and IEDS has its strengths and limitations. However, when the payoff is binary, e.g., whether a goal is satisfied, IEDS has more distinguishing power than NE. In this work, we propose Strategy Logic with IEDS (SL_{IEDS}), an extension of Strategy Logic with an IEDS operator, where we can reason about rational strategies that survive IEDS. We prove that SL_{IEDS} is strictly more expressive than SL. Finally, we prove that model checking memoryless SL_{IEDS} is EXPTIME-complete.

Coordination and joint ability are important topics in representation and reasoning about multi-agent systems. The modal logic JAADL proposed by Liu et al. extends ATL with joint abilities, which enables reasoning about whether a coalition of agents can coordinate and achieve a goal without communication. However, like ATL, strategic abilities in JAADL are defined in terms of combinatorial strategies, which are functions from histories or states to actions. On the other hand, there has been research on reasoning about natural strategic abilities, where a natural strategy is formalized as a sequence of condition-action pairs, making it more human-friendly than combinatorial strategy. In this work, we propose SJAADL, a variation of JAADL where strategic abilities are defined in terms of structured strategies represented with LDL (linear dynamic logic) formulas, with bounded complexity. We use nondeterministic strategies since they are more expressive, natural and succinct than determinstic ones. We present syntax and semantics of SJAADL. We show that model checking SJAADL can be done in time quasi-polynomial with the model size, exponential with the formula size, and with the complexity bound of structured strategies, exponential in the memoryless case and double exponential in the memoryful case. Finally, we introduce the problem of synthesizing norms to achieve joint abilities, and give two algorithms for it.