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.