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.
Continuous-time Markov decision process are an important variant of labelled transition systems having nondeterminism through labels and stochasticity through exponential firetime 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 infinite 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 finally show that each probability measure on the sigma-algebra of infinite paths is indeed induced by a measurable scheduler which proves that this class is complete.
de una red de comunicaciones para el caso de eventos raros”
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).
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.
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.
….
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
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.