References

Current needs in the verification of systems evolve from boolean properties to finer quantitative properties. The overall theory behind automatic verification is actively being extended by the scientific community from the boolean to the quantitative setting. One of the foremost extension concerns the study of probabilistic systems or probabilistic specifications. In this internship, we mainly focus on probabilistic specification formalisms. In the boolean case, a specification will assign true or false to each possible behavior. In the probabilistic extension, the specification assigns probabilities to behaviors. Recently, a fragment of weighted regular expressions was proposed and shown to have the same expressive power as probabilistic automata [1] and [3, Chapter 8]. Since the definition of these probabilistic expressions uses rewriting rules, it is not obvious to decide whether a given weighted expression is actually a probabilistic one. Solving this problem is the first aim of this internship. A second objective is to search an equivalent definition of probabilistic expression for which membership would be easier to check. There are other interesting specification formalisms, and in particular those like PDL (Propo-sitional Dynamic Logic) that mix state formulæ with path regular expressions. A weighted ex