Reachability Computation and Parameter Synthesis for Polynomial Dynamical Systems

Calcul d'atteignabilité et synthèse de paramètres pour systèmes dynamiques polynomiaux Les systèmes dynamiques sont des importants modèles mathématiques utilisés pour décrire l'évolution temporelle des systèmes.Souvent, les systèmes dynamiques sont équipées avec des paramètres qui permettent les modèles de mieux saisir les caractéristiques des phénomènes abstraits. Une question importante autour des systèmes dynamiques est de déterminer formellement si un modèle (sollicité par ses paramètres) se comporte bien.Dans cette thèse, nous traitons deux questions principales concernant les systèmes dynamiques polynomiaux en temps discret:1) problème de calcul de la d'atteignabilité, i.e., étant donné un ensemble de conditions initiales et un ensemble deparamètres, calculer l'ensemble des états atteignable par le système dans un horizon de temps borné;2) le problème de la synthèse de paramètre, i.e., étant donné un ensemble de conditions initiales,un ensemble de paramètres, et une spécification, trouver l'ensemble de paramètres le plus grandtels que tous les comportements du système fixes de l'ensemble de conditions initiales satisfont la spécification.Le problème de calcul d'atteignabilité pour les systèmes dynamiques non linéaires est bien connu pour être non triviale.Des difficultés surgissent dans le traitement et la représentation des ensembles générés par les transformations non linéaires.Dans cette thèse, nous adoptons une technique courante qui consistede rapprocher les ensembles atteignable avec des ensembles complexes qui sont faciles à manipuler.Le défi est de déterminer précis sur-approximations.Nous proposons des méthodes pour rapprocher finement les images des ensembles utilisant des boîtes,parallelotopes, et une nouvelle structure appelé parallelotope bundle (ce sont des collections de parallelotopes dont les intersections représentent symboliquement polytopes). Ces techniques d'approximation sont les étapes de base de notre algorithme d'accessibilité.La synthèse des paramètres vise à déterminer les valeursdes paramètres tels que le système se comporte comme prévu. Cette fonctionnalité peut êtreutilisé, par exemple, pour régler un modèle qu'il imite la modéliséphénomène avec un niveau suffisant de précision. Les contributions de cettethèse sur le problème de synthèse de paramètres sont de deux ordres. Premièrement,nous définissons une nouvelle sémantique pour le signal logique temporelle (STL) que nous permetde formaliser une spécification et de raisonner sur des ensembles de paramètres et des flux de comportements.Deuxièmement, nous définissons un algorithme pour calculer la sémantique de synthèsed'une formule à l'encontre d'un système dynamique à temps discret. Le résultat de l'algorithmeconstitue une solution conservatrice du problème de la synthèse de paramètre.Les méthodes développées exploitent et améliorent le calcul des coefficients de Bernstein.Les techniques définies dans cette thèse ont été mises en œuvreun tool appelé Sapo. L'efficacité de notre méthode est validéepar l'application de notre tool pour plusieurs systèmes dynamiques polynomiaux.