Difference between revisions of "Publications/gillard.18.seminar/fr"
From LRDE
(Created page with "{{CSIReportFR | authors = Clément Gillard | titre = Recherche de chemin acceptant bi-bande dans Spot | year = 2018 | number = 1805 | resume = Dans un précédent rapport nous...") |
|||
| Line 4: | Line 4: | ||
| year = 2018 |
| year = 2018 |
||
| number = 1805 |
| number = 1805 |
||
| − | | resume = Dans un précédent rapport nous présentions le test de vacuité bi-bande dans la bibliothèque Spot, qui vérifie que l'intersection des langages de deux ω-automates est vide sans construire leur |
+ | | resume = Dans un précédent rapport nous présentions le test de vacuité bi-bande dans la bibliothèque Spot, qui vérifie que l'intersection des langages de deux ω-automates est vide sans construire leur produitce qui permet de contourner une limitation de Spot sur le nombre d'ensembles d'acceptations de ces automates. Cette opération, lorsque l'intersection n'est effectivement pas vide, est généralement suivie d'une recherche de chemin acceptant sur le produit qui expose un mot qui se trouve dans les langages des deux automates. Nous présentons une nouvelle fonction qui réalise cette recherche de chemin acceptant à partir des données générées par le test de vacuité bi-bande, ce qui nous permet d'utiliser ces nouvelles méthodes dans des algorithmes qui nécessitent la recherche d'un contre-exemple. |
| type = techreport |
| type = techreport |
||
| id = gillard.18.seminar |
| id = gillard.18.seminar |
||
Latest revision as of 17:16, 6 June 2018
- Auteurs
- Clément Gillard
- Type
- techreport
- Année
- 2018
- Numéro
- 1805
Résumé
Dans un précédent rapport nous présentions le test de vacuité bi-bande dans la bibliothèque Spot, qui vérifie que l'intersection des langages de deux ω-automates est vide sans construire leur produitce qui permet de contourner une limitation de Spot sur le nombre d'ensembles d'acceptations de ces automates. Cette opération, lorsque l'intersection n'est effectivement pas vide, est généralement suivie d'une recherche de chemin acceptant sur le produit qui expose un mot qui se trouve dans les langages des deux automates. Nous présentons une nouvelle fonction qui réalise cette recherche de chemin acceptant à partir des données générées par le test de vacuité bi-bande, ce qui nous permet d'utiliser ces nouvelles méthodes dans des algorithmes qui nécessitent la recherche d'un contre-exemple.