Difference between revisions of "Publications/carvalho.20.seminar/fr"
From LRDE
(Created page with "{{CSIReportFR | authors = Thomas De Carvalho | titre = ... Insert a title in French here ... | year = 2020 | number = 2001 | resume = ... Insert an abstract in French here ......") |
|||
| Line 4: | Line 4: | ||
| year = 2020 |
| year = 2020 |
||
| number = 2001 |
| number = 2001 |
||
| + | | resume = La vérification de modèle vise à vérifier qu'un système répond à la spécification donnée en explorant tous ses états possibles. Pour y parvenir, il existe plusieurs techniques. Le Multi-Core Nested Depth-First Search (CNDFS) a un faible besoin en mémoire et fonctionne bien avec les automates de Büchi les plus simples. La Multi-Core On-The-Fly SCC Decomposition (UFSCC) a un besoin en m'moire plus important et fonctionne bien avec les automates de Büchi généralisés. La méthode symbolique a un besoin en mémoire plus faible mais dépend beaucoup de l'ordre des variables. Les performances de ces algorithmes peuvent être très différentes et choisir le meilleur en fonction d'un modèle spécifique sans les tester tous n'est pas quelque chose de facile. Ici, nous essayons d'utiliser de l'apprentissage automatisé pour prédire la meilleure méthode à utiliser pour un modèle donné. Pour cela, nous formons une forêt aléatoire, une méthode d'apprentissage d'ensemble qui utilise une multitude d'arbres de décisionen utilisant seulement les premiers états de l'espace d'état. |
||
| − | | resume = ... Insert an abstract in French here ... |
||
| type = techreport |
| type = techreport |
||
| id = carvalho.20.seminar |
| id = carvalho.20.seminar |
||
Revision as of 01:42, 27 January 2020
- Auteurs
- Thomas De Carvalho
- Type
- techreport
- Année
- 2020
- Numéro
- 2001
Résumé
La vérification de modèle vise à vérifier qu'un système répond à la spécification donnée en explorant tous ses états possibles. Pour y parvenir, il existe plusieurs techniques. Le Multi-Core Nested Depth-First Search (CNDFS) a un faible besoin en mémoire et fonctionne bien avec les automates de Büchi les plus simples. La Multi-Core On-The-Fly SCC Decomposition (UFSCC) a un besoin en m'moire plus important et fonctionne bien avec les automates de Büchi généralisés. La méthode symbolique a un besoin en mémoire plus faible mais dépend beaucoup de l'ordre des variables. Les performances de ces algorithmes peuvent être très différentes et choisir le meilleur en fonction d'un modèle spécifique sans les tester tous n'est pas quelque chose de facile. Ici, nous essayons d'utiliser de l'apprentissage automatisé pour prédire la meilleure méthode à utiliser pour un modèle donné. Pour cela, nous formons une forêt aléatoire, une méthode d'apprentissage d'ensemble qui utilise une multitude d'arbres de décisionen utilisant seulement les premiers états de l'espace d'état.