Intégration de TChecker dans Spot

From LRDE

Revision as of 17:07, 9 January 2018 by Bot (talk | contribs) (Created page with "{{CSIReportFR | authors = Arthur Remaud | titre = Intégration de TChecker dans Spot | year = 2017 | number = 1712 | resume = Un automate temporisé est un ω-automate représ...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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.