Correspondence:
[‡]
Address for correspondence: Università di Napoli Federico II, Department DIETI, Via Claudio, n.21, 80125, Napoli, Italy.
Note: [*] Partially supported by the GNCS 2016 project: Logica, Automi e Giochi per Sistemi Auto-adattivi.
Note: [†] This is an extended version of the work [1] appearing in the Proc. of CILC 2015, the 30th Italian Conf. on Computational Logic.
Abstract: In game theory, deciding whether a designed player wins a game amounts to check whether he has a winning strategy. However, there are several game settings in which knowing whether he has more than a winning strategy is also important. For example, this is crucial in deciding whether a game admits a unique Nash Equilibrium, or in planning a rescue as this would provide a backup plan. In this paper we study the problem of checking whether, in a two-player reachability game, a designed player has more than a winning strategy. We investigate this question both under perfect and imperfect information about the moves performed by the players. We provide an automata-based solution that results, in the perfect information setting, in a linear-time procedure; in the imperfect information setting, instead, it shows an exponential-time upper bound. In both cases, the results are tight.
Keywords: Additional Strategies, Two-Player Reachability Games, Graded Modalities, Imperfect Information
