La complémentation d'automates de Büchi

From LRDE

Revision as of 17:07, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReportFR | authors = Guillaume Sadegh | titre = La complémentation d'automates de Büchi | year = 2009 | resume = Le model checking est un domaine de la vérification fo...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Résumé

Le model checking est un domaine de la vérification formelle permettant de vérifier le comportement d'un système à travers des formules logiques. Spot est une bibliothèque de model checking qui repose sur une des techniques du domaine : l'approche automate. Dans cette approche du model checking, le système et les formules sont représentés sous forme d'automates acceptant des mots de longueur infinie, et plus particulièrement des automates de Büchi. Spot propose de nombreux algorithmes aux utilisateurs de la bibliothèque pour manipuler ce type d'automates, en vue d'applications au model checking. Pourtant, un algorithme est manquant : celui de la complémentation d'automates de Büchi (qui produit un automate reconnaissant la négation du langage initialement reconnu). Cet algorithme est peu utilisé dans la pratique à cause de sa forte complexité, mais il ne manque pas d'intérêt du point de vue théorique. Nous présenterons une implémentation d'un tel algorithme dans Spot.