Minimisation d'automates représentant des obligations

From LRDE

Revision as of 17:02, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReportFR | authors = Felix Abecassis | titre = Minimisation d'automates représentant des obligations | year = 2010 | number = 1004 | resume = Le model checking est une d...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Résumé

Le model checking est une discipline s'intéressant à la vérification automatique de la conformité d'un système fini vis-à-vis d'une propriété. Spot est une bibliothèque de model checking basée sur une approche automate: le système à vérifier est représenté par un automate de Büchi généralisé basé sur les transitions, les propriétés sont exprimées par des formules de logique temporelle linéaire (LTL) et sont traduites en automate de Büchi. Les formules LTL peuvent être classées dans une hiérarchie selon le type de propriété qu'elles représentent. Nous étudierons le cas des formules LTL représentant des propriétés d'obligation, ces formules peuvent être reconnues par un type plus précis d'automates dont il est possible de calculer une forme minimale canonique.