IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2008 > Quantitative Model Checking Revisited: neither Decidable nor Approximable
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Pedro R. D'Argenio

martes 30 de septiembre de 2008

3:00pm Sala de Grados

Pedro R. D'Argenio, Lecturer, Universidad Nacional de Cordoba (UNC), Argentina

Quantitative Model Checking Revisited: neither Decidable nor Approximable


Quantitative model checking computes the probability values of a given property quantifying over all possible schedulers. It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other (and hence arbitrary schedulers may result too powerful). Therefore, we focus on the quantitative model checking problem restricted to distributed schedulers that are obtained only as a combination of local schedulers (i.e. the schedulers of each component) and show that this problem is undecidable. In fact, we show that there is no algorithm that can compute an approximation to the maximum probability of reaching a state within a given bound when restricted to distributed schedulers.

We will also discuss the impact of such result on the analysis of security protocols and ideas to get better overestimatios than those obtained by standard probabilistic model checking.