Intégration de TChecker dans Spot

Auteurs

Arthur Remaud

Type

techreport

Année

2017

Numéro

1712

Résumé

Un automate temporisé est un ω-automate représentant un modèle comportant des conditions de temps continu, ce qui peut aboutir à un espace d'états infini. Cependant, il est possible de le ramener à un automate fini, appelé graphe de zones, afin d'étudier ses propriétés. Dans ce rapport, nous montrons comment les automates temporisés sont intégrés à Spot. Nous utilisons TChecker, qui est un programme conc cu au LaBRI. Nous expliquons comment sont intégrés les représentations des graphes de zones qu'utilise TChecker pour travailler sur les automates temporisés dans Spot. Nous montrons ensuite comment les algorithmes de Spot lisent cette adaptation pour travailler sur des automates temporisés et des graphes de zones. Nous montrons enfin comment sont contournés certains inconvénients de TChecker afin de rendre plus simple son utilisation par Spot.