Vérification de spécifications temporelles linéaires sur les systèmes multimodes à taux constant

Abstract

Les systèmes multimodes à taux constant (MMS) sont des systèmes hybrides avec un nombre fini de modes et des variables réelles qui évoluent dans le temps continu selon des taux constants spécifiques à chaque mode. Nous introduisons une variante de la logique temporelle linéaire (LTL) pour les MMS, et nous étudions la complexité calculatoire du problème qui consiste à déterminer si un MMS donné satisfait une spécification LTL donnée. Nous obtenons un paysage de complexité où chaque fragment syntaxique de LTL est soit P-complet, soit NP-complet, soit indécidable. Ces résultats généralisent et unifient plusieurs résultats sur les MMS et les systèmes à compteurs continus.