The paper "The Complexity of LTL Rational Synthesis" by Orna Kupferman and Noam Shenwald explores the complexity of constructing a reactive system that satisfies its specification in all rational environments, where the environment has objectives and acts to fulfill them. The authors make three main contributions:
1. **Tightening Known Upper Bounds**: They improve the known upper bounds for settings that were previously left open, particularly for games with three or more players and concurrent games.
2. **Parametric Complexity Analysis**: They provide tight upper and lower bounds in each of the problem parameters: the game graph, the objectives of the system components, and the objectives of the environment components.
3. **Generalization of Rational Synthesis**: They generalize the definition of rational synthesis by adding hostile players and combining cooperative and non-cooperative approaches.
The paper focuses on two types of rational synthesis: cooperative rational synthesis (CRS) and non-cooperative rational synthesis (NRS). CRS aims to find a strategy for controllable players such that the objectives of controllable players are satisfied in every Nash equilibrium profile, while NRS seeks a strategy for the system player that ensures the system's objective is met in all Nash equilibria.
The authors reduce the problem of rational synthesis to the nonemptiness problem of tree automata, which accept certified strategy trees. They construct automata that check if a profile tree is a solution to the problem, with the size of the automata depending on the parameters of the problem. They also provide tight lower bounds for the complexity of CRS and NRS, showing that they are EXPTIME-hard in certain cases.
Additionally, the paper introduces the concept of uncontrollable hostile players, which are similar to traditional hostile players but do not have an objective. The authors show that these players can be viewed as rational players whose objectives complement the system's objective.
Overall, the paper completes the complexity analysis of LTL rational synthesis, providing a comprehensive understanding of the computational complexity of the problem in various settings.The paper "The Complexity of LTL Rational Synthesis" by Orna Kupferman and Noam Shenwald explores the complexity of constructing a reactive system that satisfies its specification in all rational environments, where the environment has objectives and acts to fulfill them. The authors make three main contributions:
1. **Tightening Known Upper Bounds**: They improve the known upper bounds for settings that were previously left open, particularly for games with three or more players and concurrent games.
2. **Parametric Complexity Analysis**: They provide tight upper and lower bounds in each of the problem parameters: the game graph, the objectives of the system components, and the objectives of the environment components.
3. **Generalization of Rational Synthesis**: They generalize the definition of rational synthesis by adding hostile players and combining cooperative and non-cooperative approaches.
The paper focuses on two types of rational synthesis: cooperative rational synthesis (CRS) and non-cooperative rational synthesis (NRS). CRS aims to find a strategy for controllable players such that the objectives of controllable players are satisfied in every Nash equilibrium profile, while NRS seeks a strategy for the system player that ensures the system's objective is met in all Nash equilibria.
The authors reduce the problem of rational synthesis to the nonemptiness problem of tree automata, which accept certified strategy trees. They construct automata that check if a profile tree is a solution to the problem, with the size of the automata depending on the parameters of the problem. They also provide tight lower bounds for the complexity of CRS and NRS, showing that they are EXPTIME-hard in certain cases.
Additionally, the paper introduces the concept of uncontrollable hostile players, which are similar to traditional hostile players but do not have an objective. The authors show that these players can be viewed as rational players whose objectives complement the system's objective.
Overall, the paper completes the complexity analysis of LTL rational synthesis, providing a comprehensive understanding of the computational complexity of the problem in various settings.