4 avril 2016
Rodica Bozianu (LACL)In this paper, we study the computational complexity of the cooperative and non-cooperative rational synthesis problems, as introduced by Kupferman, Vardi and coauthors in recent papers for general LTL objectives. From the previous papers we get that the cooperative and non-cooperative rational synthesis problems are 2ExpTime-complete for specifications expressed in linear temporal logic (LTL), thus matching exactly the complexity of classical zero-sum two-player LTL synthesis.
We investigate these problems on multiplayer turn-based games played on graphs, and provide complexity results for the classical omega-regular objectives, namely reachability, Safety, Buchi, coBuchi, parity, Rabin, Streett and Muller objectives. Most of these complexity results are tight and shed light on how to solve those problems optimally.
We also study the computational complexity of solving those games when the number of players is fixed. This parametrized analysis makes sense as the number of components forming the environment may be limited in practical applications.
Joint work with Emmanuel Filiot, Raffaella Gentilini et Jean-François Raskin