Traduction efficace de formules LTL d'équité en automates déterministes

Auteurs

Laurent XU

Type

techreport

Année

2018

Numéro

1802

Résumé

En vérification formelle de la logique temporelle linéaire (LTL) à l'aide d'ω-automates, la négation d'une formule LTL est traduite en ω-automate. La construction d'un automate plus petit réduit beaucoup le temps d'exécution et la consommation mémoire des opérations suivantes de la chaîne de traitement de la vérification formelle. Müller et Sickert ont présenté une méthode efficace pour traduire n'importe quelle formule LTL en un petit automate déterministe. Cette méthode consiste à découper la formule en trois ensembles de sous-formules qui appartiennent respectivement au fragment de sureté ou de garantie, au fragment d'équité et au reste. Ils traduisent ensuite individuellement ces ensembles de sous-formules en automates déterministes qu'ils combinent par la suite. Spot peut déjà traduire les formules d'obligation en automates déterministes minimaux. Les formules d'obligation étant un surensemble des formules de sureté et de garantie, on généralise la traduction de Müller et Sickert en remplaçant le fragment de sureté ou de garantie par le fragment d'obligation. En ce qui concerne le fragment d'équité, ils ont présenté un algorithme de traduction efficace qui produit de petits automates déterministes. Ils ont également présenté comment construire efficacement un produit de ces automates avec d'autres automates. Nous présentons comment nous implémentons ces deux méthodes dans Spot.