DI-UMONS : Dépôt institutionnel de l’université de Mons

Recherche transversale
Rechercher
(titres de publication, de périodique et noms de colloque inclus)
2014-04-24 - Travail avec promoteur/Doctorat - Anglais - 330 page(s)

Randour Mickaël , "Synthesis in Multi-Criteria Quantitative Games", Bruyère Véronique , Raskin Jean-François, 2010-10-01, soutenue le 2014-04-24

  • Edition : UMONS
  • Codes CREF : Logique mathématique (DI1170), Théorie des algorithmes (DI1164), Informatique mathématique (DI1160), Informatique générale (DI1162), Théorie de la décision et des jeux (DI1134)
  • Jury : Bouyer-Decitre Patricia, Brihaye Thomas (p) , Bruyère Véronique , Henzinger Thomas A., Raskin Jean-François, Katoen Joost-Pieter, Mélot Hadrien
  • Unités de recherche UMONS : Informatique théorique (S829)
  • Instituts UMONS : Institut de Recherche en Technologies de l’Information et Sciences de l’Informatique (InforTech), Institut de Recherche sur les Systèmes Complexes (Complexys)
  • Centres UMONS : Modélisation mathématique et informatique (CREMMI)
Texte intégral :

Abstract(s) :

(Anglais) 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.


Mots-clés :
  • (Anglais) stochastic models
  • (Anglais) Markov decision processes
  • (Anglais) multi-dimension games
  • (Anglais) quantitative models
  • (Anglais) weighted games
  • (Anglais) computer-aided verification and synthesis
  • (Anglais) window games
  • (Anglais) game theory
  • (Anglais) formal methods
  • (Anglais) complex systems