Abstract :
[en] Verification and synthesis are successful applications of computer science, based on extensive formal bases. Model checking is supported by powerful tool suites and is now an essential part of many high-end industrial processes. Synthesis is promising and should have important long-term impact.
One of the crucial changes over the last decade is the evolution from Boolean to quantitative specifications, giving more expressive models that describe quality of service or performance of systems. However, current models cannot account for trade-offs and interplays between quantitative aspects, which naturally arise in many applications. This thesis participates in the shift from single-criterion quantitative models toward multi-criteria ones. Our study is focused on the game-theoretic framework, modeling the interactions between a reactive system and its environment as a competitive two-player game.
Our contributions are of two kinds. On the one hand, we obtain new results on existing models and improve their tractability. On the other hand, we introduce novel models with interesting properties. Questions we address include deciding the winner in games with rich winning objectives, establishing efficient synthesis algorithms, bounding the memory needs for strategies, and other related problems.
We cover three axes of research. First, we study games with multi-dimension quantitative objectives. We prove surprising complexity results for the total-payoff and establish an optimal synthesis algorithm for mean-payoff and energy objectives along with a parity condition. Second, we introduce window objectives, which provide a framework to reason about quantitative behaviors in time frames. Those new objectives also approximate classical ones while avoiding a long-standing complexity barrier. Finally, we develop the novel concept of beyond worst-case synthesis, combining worst-case and expected value requirements for synthesized system controllers. We study it for two important quantitative settings: mean-payoff and shortest path. For the former, we show that it provides additional expressive power for free complexity-wise.
