Multi-weighted Reachability Games and Their Application to Permissiveness

TL;DR

This paper investigates multi-weighted reachability games on finite graphs, focusing on strategy synthesis and complexity analysis for optimizing cost profiles under different orderings, with applications to permissiveness.

Contribution

It introduces a fixpoint algorithm for synthesizing lexicographic and Pareto-optimal strategies and analyzes their computational complexity.

Findings

Polynomial-time computation of the upper value for lexicographic order.

Exponential-time computation of the Pareto frontier.

Complexity results for the constrained existence problem under different orders.

Abstract

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. Cost profiles are compared thanks to: (i) a lexicographic order that ensures the unicity of an upper value and (ii) a componentwise order for which we consider 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. The constrained existence problem is proved in P for the lexicographic order and PSPACE-complete for the componentwise order. Finally, we show how complexity results about permissiveness of multi-strategies in two-player quantitative reachability games can be derived from the results we obtained in the two-player multi-weighted reachability games setting.