Reasoning about temporal properties of rational play (Q1028639)

The paper proposes and studies an extension of the Alternating-Time Temporal Logic (\(\mathbf {ATL}\)), called \(\mathbf {ATLP}\) (\(\mathbf {ATL}\) with plausibility), that makes it possible to express various rationality assumptions of intelligent agents and reasoning about agents' abilities to achieve formally specified outcomes under such rationality assumptions on their strategies. In particular, the authors show that various classical solution concepts, such as standard and subgame perfect Nash equilibria, Pareto-optimality, etc., can be characterized in \(\mathbf {ATLP}\), and the resulting behaviours and outcomes can then be formally analyzed. The logic also gives rise to generalized versions of classical solution concepts through characterizing patterns of payoffs by path formulae of \(\mathbf {ATL}\). The paper investigates the complexity of model checking \(\mathbf {ATLP}\) for several classes of formulae, and shows that it ranges from \(\Delta_{\mathbf{3}}^{\mathbf{P}}\) to \(\mathbf {PSPACE}\) in the general case and from \(\Delta_{\mathbf{3}}^{\mathbf{P}}\) to \(\Delta_{\mathbf{4}}^{\mathbf{P}}\) for the most interesting subclasses, and roughly corresponds to solving extensive games with imperfect information.