Séminaires
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:
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: Le 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.