Séminaire du 4 Novembre 2011

Lieu

LACL: comment y aller
Salle des thses, Bat. P (Faculté des Sciences et Technologie) rez de chaussée.

Programme

14h00-15h00: K. Klai, LIPN - Université Paris 13, "Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking", joint work with A. Duret-Lutz, D. Poitrenaud, and Y. Thierry-Mieg

Abstract:transparents We present two new hybrid techniques that replace the synchronized  product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates  (symbolic sets of states) that can be interpreted as Büchi  automata. These hybrid approaches allow on the one hand to use classical emptiness-check algorithms and to build the graph on-the-fly,  and on the other hand, to have a compact encoding of the state space  thanks to the symbolic representation of the aggregates.  The  Symbolic Observation Product (SOP) assumes a globally stuttering property (e.g., LTL\X) to aggregate states.  The  Self-Loop Aggregation Product (SLAP) does not require the property to be globally stuttering (i.e., it can tackle full LTL), but dynamically detects and exploits a form of stuttering where possible.  Our experiments show that these two variants, while incomparable with each other, can outperform other existing approaches.

15h00-15h30 : B. Barbot, LSV - ENS de Cachan, "échantillonnage préférentiel pour le model-ckecking statistique", travail en commun avec S. Haddad et C. Picaronny

Abstract: transparentsLe model checking statistique est une alternative intéressante au model checking numérique lorsque les modèles probabilistes étudiés sont de très grande taille. Cependant l'approche statistique ne permet pas d'évaluer les probabilités des évènements rares. Afin de résoudre ce problème, nous développons ici une nouvelle approche basée sur l'échantillonnage préférentiel. Alors que la plupart des techniques d'échantillonnage préférentiel sont basées sur des heuristiques, nous établissons des résultats théoriques. Moyennant certaines hypothèses, ces résultats garantissent une réduction de la variance lors de l'application de l'échantillonnage préférentiel. Nous caractérisons des situations qui vérifient les hypothèses et étendons notre approche dans les autres situations mais cette fois-ci sans garantie théorique. Nous avons implémenté cette approche à l'aide de l'outil Cosmos après avoir ajouté des fonctionnalités. Enfin nous présentons l'évaluation de notre méthode sur deux exemples et analysons les expérimentations.

15h30-16h00: pause café

16h00-16h30: vie du groupe