• QUAVERIF is an international bilateral project between LSV, ENS Cachan (France) and the group of Formal Methods and Verification, ULB (Belgium), funded by CNRS (Centre National de la Recherche Scientifique) through the PICS programme (Projets internationaux de coopération scientifique).

 Keywords

• Quantitative Verification
• Stochastic Games
• Algorithms and Complexity

 Description

• The project lies in the field of formal methods and verification of computer systems. We focus on reactive computer systems with stochastic behaviors, and study new approaches to the quantitative verification of such systems. We define new quantitative properties and semantics, and look after their theoretical facets including closure properties, computational complexity and expressive power. In particular, we study stochastic games which provides a rich mathematical framework to model various kinds of behaviors and interactions. We define new quantitative objectives for these games, and we study the complexity and algorithms for their decision problems (existence and construction of optimal strategies).

 Participants

• Laurent Doyen (LSV, Principal Investigator)
• Thierry Massart (ULB)
• Mahsa Shirmohammadi (PhD student)

 Schedule

• Starting date: February 15th, 2013
• Duration: 3 years

 Publications

• Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Limit Synchronization in Markov Decision Processes. Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Lecture Notes in Computer Science 8412, Springer, 2014, pp. 58-72.

• Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Robust Synchronization in Markov Decision Processes. Proceedings of the 25th International Conference on Concurrency Theory (CONCUR), Lecture Notes in Computer Science 8704, Springer, 2014, pp. 234-248.

• Laurent Doyen, Line Juhl, Kim G. Larsen, Nicolas Markey, and Mahsa Shirmohammadi. Synchronizing Words for Weighted and Timed Automata. Proceedings of the 34h International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014, pp. 121-132.

 Related Work

• Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Infinite Synchronizing Words for Probabilistic Automata. Proceedings of the 36th International Symposium on Mathematical Foundations of Computer Science (MFCS), Lecture Notes in Computer Science 6907, Springer, 2011, pp. 278-289.

• Laurent Doyen, Thierry Massart, and Mahsa Shirmohammadi. Synchronizing Objectives for Markov Decision Processes. Proceedings of International Workshop on Interactions, Games and Protocols (iWIGP), Electronic Proceedings in Theoretical Computer Science 50, 2011, pp. 61-75.