Un cadre entièrement automatisé pour le contrôle des systèmes linéaires à partir de spécifications en logique temporelle

Nous considérons le problème suivant : étant donné un système linéaire et une formule de logique temporelle linéaire (LTL) sur un ensemble de prédicats linéaires dans ses variables d'état, trouver une loi de contrôle rétroaction avec des bornes polyédriques et un ensemble d'états initiaux de sorte que toutes les trajectoires du système en boucle fermée satisfassent la formule. Notre solution à ce problème se compose de trois étapes principales. Tout d'abord, nous partitionnons l'espace d'état en accord avec les prédicats de la formule et construisons un système de transition sur le quotient de la partition, qui capture notre capacité à concevoir des contrôleurs. Deuxièmement, en utilisant une procédure ressemblant à la vérification de modèle, nous déterminons les trajectoires du système de transition satisfaisant la formule. Troisièmement, nous générons la stratégie de contrôle. Des exemples illustratifs sont inclus.