Enhancing Strategy Logic with Procedural Rationality

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.