Artificial states generation in state spaces using kernel density estimation

From LRDE

Revision as of 17:22, 9 November 2020 by Bot (talk | contribs)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Résumé

L'objectif est d'améliorer Spot, une bibliothèque de Model Checking. Spot utilise un type de graphe spécifique dans lequel chaque état est un ensemble de variables avec des valeurs données. Ces valeurs peuvent être vues comme des coordonnées et un état peut donc être vu comme un point à N dimensions. L'espace d'états est alors un nuage à N dimensions et Spot effectue un parcours en profondeur sur celui-ci. Nous voulons générer des états à la volée pour améliorer les performances. Pour cela, nous utilisons une estimation de densité de probabilité par noyau. Les états générés sont ensuite utilisés comme points de départ pour des processus qui exploreront l'espace d'états en parallèle.