Conferencia invitada en el 11º ERPEM
El Encuentro Regional de Probabilidades y Estadística, es un encuentro anual que se realiza en la región con el fin de promover interacciones entre estudiantes, jóvenes investigadores y expertos de la región en el área de Probabilidades y Estadística, para fomentar nuevas interacciones y colaboraciones facilitando desde las instituciones involucradas el intercambio de ideas por medio de discusiones informales.
En esta 11º edición, a los organizadores, encabezado por Marcelo Ruíz (UNRC), les picaron las ganas de saber que era eso de Probabilistic Model Checking y decidieron invitarme a dar una charla. Traté de no aburrirlos (pueden ver las filminas adjuntas), y la verdad que la pasé bárbaro.
Así que vaya mi agradecimiento a toda la gente del 11º ERPEM, también a la de los Departamento de Matemáticas y de Computación de la UNRC, y en particular a Marcelo Ruiz.
Titulo de la charla: An Introduction to Probabilistic Model Checking.
Resumen: Probability is an important aspect on the design and analysis of algorithms, specially when they interact with the physical media. On the one hand, it is common that distributed algorithms take decisions based on coin tossing in order to achieve more efficient solutions, or even some solution when otherwise would not have been possible. Examples of this case can be found on the wired or wireless network protocols that we use every day (namely, Ethernet and the IEEE 802.11 family). On the other hand, external events can be quantified probabilistically, e.g., the ratio of messages lost in a wireless medium, the average time of a client component accessing a file server, etc. Thus, the verification and analysis of this type of algorithms should not neglect the influence of the random components. Probabilistic Model Checking provides an automatic technique for the analysis and verification of systems that exhibit random or probabilistic behaviour as well as non-deterministic behaviour. In this talk, I will provide some motivation for the need of this type of techniques, as well as give an overview of the foundations of probabilistic model checking.