Generalized Reachability Games Are PSPACE-Complete, New Proof Shows

In classic reachability games, one player (Eve) aims to visit a single target set while the opponent (Adam) tries to prevent it. The new paper generalizes this to multiple target sets, where Eve must visit all of them (in any order) to win. The authors, led by Sougata Bose and Nathanael Fijalkow, analyze the computational complexity of determining the winner in these generalized reachability games. Their first key result is a tight PSPACE-completeness classification: deciding the winner is PSPACE-hard even when each target set has at most three vertices, and the problem belongs to PSPACE for target sets of arbitrary size.

Beyond the worst-case hardness, the paper reveals fixed-parameter tractability (FPT) when parameterized by the number of target sets that contain more than one vertex. They also provide matching upper and lower bounds on the memory required for winning strategies for both players. For optimization variants, the picture is largely bleak: maximizing the number of visited target sets is coNP-hard. However, tractability returns in a “pledge” setting where Eve commits to a maximum subset she can guarantee. These results have immediate implications for formal verification, AI planning, and any domain requiring multi-objective reasoning under adversarial dynamics.