Towards parameterized verification of probabilistic systems.

On the one hand, model-checking of finite probabilistic systems (Markov chains and Markov decision processes) is now well-established. The traditional questions concern the verification of these models against probabilistic logics. We distinguish qualitative questions --that compare probabilities to the extreme values 0 and 1-- and quantitative ones --for which the thresholds are arbitrary.

On the other hand, parameterized verification (dating back the 80's) aims at checking at once many instances of a problem. This reasoning is typically useful when one considers protocols that execute over networks of many identical processes: one wants to verify the protocol for all possible number of processes. As an example, parameterized verification has been recently studied in the context of ad hoc networks.

We will start the talk by reviewing fundamental results about probabilistic model-checking of finite state systems. Then, we will expose the problem of parameterized verification of probabilistic systems and provide preliminary results on the subject.