¡Esta es una revisión vieja del documento!
= 28 de agosto =
Seminario de Ciencias de la Computación. En cumplimiento de los requerimientos del doctorado.
Martes 28, 16:00 hs. Aula Smith (Aula Grupo de Computación)
Expositor: Sergio Giro
Título: Una revisión del model checking cuantitativo: ni decidible ni aproximable.
Resumen:
En el model checking cuantitativo se calcula la probabilidad de una propiedad variando sobre todos los schedulers posibles. A menudo, las probabilidades máximas y minimas calculadas de esta forma son sobreestimaciones si las componentes del sistema tienen pocas interacciones o comparten poca información (en estos casos los schedulers pueden “adivinar” información oculta por otra componente). En este trabajo nos enfocamos en el problema de model checking cuantitativo cuando, en lugar de considerar todos los schedulers, se consideran sólo los schedulers distribuidos que resultan de la composición de schedulers locales (es decir, schedulers para una componente determinada) y mostramos que este problema es indecidible. Llegamos a esta conclusión mostrando que no existe ningún algoritmo que pueda calcular una aproximación de la probabilidad máxima (considerando sólo los schedulers distribuidos) de alcanzar un estado.
Lunes 10 de Septiembre Chun
Titulo: “Algoritmos eficientes para la estimación de la confiabilidad de una red de comunicaciones para el caso de eventos raros”
Resumen:
Un evento raro, es un evento que tiene una probabilidad de un orden menor que 10-9. Muchas veces calcular la probabilidad del evento resulta imposible por la complejidad del sistema, cuando esto ocurre se recurre al Método de Monte Carlo. Pero cuando nos encontramos en el caso de los “eventos raros”, las técnicas de simulación se encuentran con importantes dificultades, ya que la baja probabilidad del evento de interés hace imposible observarlo en una evolución aleatoria del sistema. Esto genera una baja precisión del estimador y una gran cantidad de experimentos no significativos. Para hacer frente a estos problemas se han desarrollados distintas técnicas, algunas de estas se enfocan en mejorar la precisión del algoritmo de simulación, recurriendo a algoritmos más complejos, lo cual significa, en algunos casos, un mayor tiempo computacional. En otros casos, se recurre a algoritmos con igual precisión por replicación que el método Monte Carlo pero con un menor costo computacional.
En esta charla trataremos el problema de estimar la probabilidad de conectar dos nodos de un grafo no dirigido, el cual representa un red de comunicaciones donde los nodos son perfectos pero las lineas pueden fallar. Se presentará un algoritmo que ahorra un mayor tiempo computacional a medida que decrece la probabilidad del evento “no se puede conectar los dos nodos”. Además se verá como lograr una menor varianza, con una pequeña modificación al algoritmo. Habrá una rápida introducción al método “Randomized Quasi Monte Carlo”, una técnica para reducir la varianza, y los resultados obtenidos al utilizarlo en nuestro algoritmo modificado. Por último se aplicará un enfoque distinto para atacar el problema, este nuevo enfoque se basa en los estimadores de varianza cero (zero-variance estimator).
8 de octubre de 2007 Expositor: Javier.
¿De qué habla la Informática? Javier Blanco
Existen diversas maneras de concebir a la informatica y algunas de dichas concepciones son incompatibles entre si. Las discrepancias se presentan tanto explícita como implícitamente y abarcan cuestiones ontológicas, epistemológicas y metodoloógicas. Comprender bien estas disputas filosóficas puede tener consecuencias drásticas en los diferentes ámbitos de desarrollo de esta disciplina. En la charla se expondrán las características principales de las diferentes concepciones y se propodrá la apertura de un necesario y postergado diálogo.
16 de octubre de 2007 Damian, parte seminario.
Titulo: Generación de invariantes para implementar eficientemente Regiones Críticas Condicionales
Abstract: La técnica de semáforos binarios divididos (SBS) puede ser usada para implementar regiones críticas condicionales. Dada una especificación de un problema de esta clase, SBS brinda tanto los programas que lo implementan como los invariantes que aseguran su corrección. Aplicando la técnica a casos particulares se encuentran programas que admiten simplificaciones.
Este trabajo se concentra en el desarrollo de un procedimiento automático para obtener estas simplificaciones. El procedimiento consiste en hacer una búsqueda de nuevos invariantes que avalen la corrección de las simplificaciones. Para esto usamos técnicas de generación de invariantes, en particular propagación hacia atrás de las precondiciones más débiles. Su implementación fue realizada utilizando los demostradores Isabelle/HOL y CVC~Lite para las demostraciones de validez y simplificaciones de las fórmulas lógicas envueltas en el proceso. El método fue probado sobre diferentes ejemplos clásicos de programación concurrente.
5 de Noviembre de 2007
Charla de Renato
….
26 de Noviembre de 2007
Saludos Gente, para este lunes ya tenemos expositior: Miguel Andrés. Miguel se recibio de la Lic. el año pasado y ahora se encuentra en Holanda realizando su doctorado. El titulo de la charle es: “CONDITIONAL PROBABILITIES OVER PROBABILISTIC AND NONDETERMINISTIC SYSTEMS.”
El paper se puede acceder en http://www.cs.ru.nl/M.Andres/index.html
Como siempre a las 9.30 en la salita Smith.
Me despido dejando el Abstract.
ABSTRACT
This work introduces the logic cpCTL, which extends the probabilistic temporal logic pCTL with conditional probability, allowing one to express that the probability that phi is true given that psi is true is at least a. We interpret cpCTL over Markov Chains and Markov Decision Processes. While model checking cpCTL over Markov Chains can be done with existing techniques, but those techniques do not carry over to Markov Decision Processes. We present a model checking algorithm for Markov Decision Processes. We also study the class of schedulers that suffice to find the maximum and minimum probability that phi is true given that psi is true. Finally, we present the notion of counterexamples for cpCTL model checking and provide a method for counterexample generation.
Lunes 3 de Diciembre.
Saludos gente, este lunes la charla va a estar a cargo de la Lic. Araceli Acosta. El titulo de la misma: “Tolerancia a fallas”. Cómo siempre, a las 9.30 en la sala Smith.