Quantitative Reachability Stackelberg-Pareto Synthesis is NEXPTIME-Complete
share
In this paper, we deepen the study of two-player Stackelberg games played on graphs in which Player 0 announces a strategy and Player 1, having several objectives, responds rationally by following plays providing him Pareto-optimal payoffs given the strategy of Player 0. The Stackelberg-Pareto synthesis problem, asking whether Player 0 can announce a strategy which satisfies his objective, whatever the rational response of Player 1, has been recently investigated for ω-regular objectives. We solve this problem for weighted graph games and quantitative reachability objectives such that Player 0 wants to reach his target set with a total cost less than some given upper bound. We show that it is NEXPTIME-complete, as for Boolean reachability objectives.
READ FULL TEXT