Natural strategic ability

In game theory, as well as in the semantics of game logics, a strategy can be represented by any function from states of the game to the agent's actions. That makes sense from the mathematical point of view, but not necessarily in the context of human behavior. This is because humans are quite bad at executing complex plans, and rather unlikely to come up with such plans in the first place. A similar concern applies to artificial agents with limited memory and/or computational power. In this paper, we adopt the view of bounded rationality, and look at “simple” strategies in specification of agents' abilities. We formally define what “simple” means, and propose a variant of alternating-time temporal logic that takes only such strategies into account. We also study the model checking problem for the resulting semantics of ability. After that, we turn to the broader issue of natural strategic abilities in concurrent games with LTL-definable winning conditions, and study a number of decision problems based on surely winning and Nash equilibrium. We show that, by adopting the view of bounded rationality based on natural strategies, we significantly decrease the complexity of rational verification for multi-agent systems.