Difference between revisions of "Publications/carvalho.19.seminar/fr"
From LRDE
(Created page with "{{CSIReportFR | authors = Thomas De Carvalho | titre = Artificial states generation in state spaces using kernel density estimation | year = 2019 | number = 1916 | resume = L'...") |
|||
| Line 4: | Line 4: | ||
| year = 2019 |
| year = 2019 |
||
| number = 1916 |
| number = 1916 |
||
| − | | resume = 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. |
+ | | resume = 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. |
| type = techreport |
| type = techreport |
||
| id = carvalho.19.seminar |
| id = carvalho.19.seminar |
||
Latest revision as of 18:22, 9 November 2020
- Auteurs
- Thomas De Carvalho
- Type
- techreport
- Année
- 2019
- Numéro
- 1916
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.