Doctoral thesis (Dissertations and theses)
Synthesis in Multi-Criteria Quantitative Games
Randour, Mickaël
2014
 

Files


Full Text
thesis.pdf
Publisher postprint (1.96 MB)
Download

All documents in ORBi UMONS are protected by a user license.

Send to



Details



Keywords :
stochastic models; Markov decision processes; multi-dimension games; quantitative models; weighted games; computer-aided verification and synthesis; window games; game theory; formal methods; complex systems
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.
Research center :
CREMMI - Modélisation mathématique et informatique
Disciplines :
Computer science
Mathematics
Author, co-author :
Randour, Mickaël ;  Université de Mons > Faculté des Sciences > Informatique théorique
Language :
English
Title :
Synthesis in Multi-Criteria Quantitative Games
Defense date :
24 April 2014
Number of pages :
330
Institution :
Université de Mons
Degree :
Doctorat en sciences (sciences informatiques)
Promotor :
Bruyère, Véronique  ;  Université de Mons > Faculté des Sciences > Service d'Informatique théorique
Raskin, Jean-François
President :
Brihaye, Thomas  ;  Université de Mons > Faculté des Sciences > Mathématiques effectives
Jury member :
Bouyer-Decitre, Patricia
Bruyère, Véronique  ;  Université de Mons > Faculté des Sciences > Service d'Informatique théorique
Henzinger, Thomas A.
Raskin, Jean-François
Katoen, Joost-Pieter
Mélot, Hadrien  ;  Université de Mons > Faculté des Sciences > Algorithmique
Research unit :
S829 - Informatique théorique
Research institute :
R300 - Institut de Recherche en Technologies de l'Information et Sciences de l'Informatique
R150 - Institut de Recherche sur les Systèmes Complexes
Available on ORBi UMONS :
since 06 October 2014

Statistics


Number of views
29 (1 by UMONS)
Number of downloads
76 (1 by UMONS)

Bibliography


Similar publications



Contact ORBi UMONS