M2 Internship

Comparison of approaches to quantitative verification

Supervisors: Eugene Asarin and Aldric Degorre.

Given a system S and a property P we want to know, to which extent (how much), the behaviour of S satisfies P. Differently from the classical qualitative model-checking, the answer is a real number , not a simple yes/no.

Numerous approaches have been developed during last 10 or 15 years: probabilistic ones, simulation games, entropy-based etc.  Each of them works fine one some problems and gives  a trivial response (collapses) on others. The aim of this internship is to characterize and compare existing approaches (an/or develop new ones) in theory and in practice.