Multi-Weighted Reachability Games

We study two-player multi-weighted reachability games played on a finite directed graph, where an agent, called P1, has several quantitative reachability objectives that he wants to optimize against an antagonistic environment, called P2. In this setting, we ask what cost profiles P1 can ensure regardless of the opponent's behavior. Since this set of ensured values may not be a singleton, cost profiles are compared thanks to: (i) a lexicographic order that ranks the objectives a priori, ensuring the unicity of an upper value or (ii) a componentwise order. In the latter case, P1 chooses his ``preferred'' ensured value a fortiori, once he knows the Pareto frontier. We synthesize (i) lexico-optimal strategies and (ii) Pareto-optimal strategies. The strategies are obtained thanks to a fixpoint algorithm which also computes the upper value in polynomial time and the Pareto frontier in exponential time. Finally, we study the complexity of a related decision problem: the constrained existence problem. This problem is proved in P with the lexicographic order and PSpace-complete with the componentwise order. This is a joint work with Thomas Brihaye. Contributed talk given by Aline Goeminne

Authors

• Aline Goeminne

Keywords

No keywords are indexed for this paper.