Diferencias

Muestra las diferencias entre dos versiones de la página.

--- seminarios_de_metodos_formales:ano_2007 [2008/12/23 21:26] – creado nueces
+++ seminarios_de_metodos_formales:ano_2007 [2008/12/23 21:44] (actual) – borrado nueces
@@ Línea 1: / Línea 1: @@
-=== Martes 28 de agosto ===
-  * 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 3 de septiembre ===
-  * Expositor: Nicolás Wolovick (http://www.cs.famaf.unc.edu.ar/~nicolasw/)
-  * Título: Una caracterización de schedulers significativos para procesos de decision de Markov de tiempo continuo.
-  * Resumen:
-Continuous-time Markov decision process are an important variant of labelled transition systems having nondeterminism through labels and stochasticity through exponential ﬁretime distributions. Nondeterministic choices are resolved using the notion of a scheduler. In this paper we characterize the class of measurable schedulers, which is the most general one, and show how a measurable scheduler induces a unique probability measure on the sigma-algebra of inﬁnite paths. We then give evidence that for particular reachability properties it is sufficient to consider a subset of measurable schedulers. Having analyzed schedulers and their induced probability measures we ﬁnally show that each probability measure on the sigma-algebra of inﬁnite paths is indeed induced by a measurable scheduler which proves that this class is complete.
--------
-=== Lunes 10 de Septiembre ===
-  * Expositor: Matías Lee
-  * 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 ===
-  * Expositor: Javier Blanco
-  * Título: ¿De qué habla la Informática?
-  * Resumen:
-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 ===
-  * Expositor: Damián Barsotti
-  * Titulo: Generación de invariantes para implementar eficientemente Regiones Críticas Condicionales
-  * Resumen:
-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 ===
-  * Expositor: Renato Cherini
-....
----------
-=== 26 de Noviembre ===
-  * Expositor: Miguel Andrés
-  * Título: CONDITIONAL PROBABILITIES OVER PROBABILISTIC AND NONDETERMINISTIC SYSTEMS
-  * Resumen:
-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.
-http://www.cs.ru.nl/M.Andres/index.html
-----------
-=== Lunes 3 de Diciembre ===
-  * Expositor: Araceli Acosta
-  * Título: Traducción de fórmulas DPLT a mu-calculus
-  * Resumen:
-DPLT (Deontic propositional Logic) es una lógica dinámica proposicional que tiene operadores deónticos. Éstos nos permiten expresar con facilidad cierto tipo de propiedades; utilizadas, por ejemplo, para especificar sistemas tolerantes a fallas.
-Nuestra motivación para definir una traducción automática para este tipo de fórmulas a mu-calculus radica en la existencia de algoritmos de model checking desarrollados para mu-calculus. Esto nos permite definir una herramienta de model checking para DPLT, de manera indirecta.