Ce module offre une introduction concise aux espaces vectoriels normés et aux concepts de stabilité dans les systèmes autonomes, englobant à la fois la stabilité asymptotique et la stabilité asymptotique globale. Il met l'accent sur l'application du théorème de stabilité de Lyapounov pour la vérification formelle de ces propriétés dans les systèmes complexes, y compris son application à divers systèmes simples, tels que les systèmes linéaires. A travers des exemples illustratifs, nous démontrerons l'importance de ces concepts dans l'analyse et la garantie de la stabilité des systèmes.

Plongez dans le sujet des ensembles atteignables et découvrez leur rôle critique dans la garantie de la sécurité des systèmes. Ce module introduit des cadres pour explorer les techniques de calcul pour sur-approximer les ensembles atteignables dans diverses classes de systèmes. Vous aurez l'occasion d'appliquer vos connaissances dans des contextes réels, d'étudier l'utilisation des zonotopes et de reconnaître leurs propriétés bénéfiques dans le calcul des ensembles atteignables. De plus, nous approfondissons les concepts fondamentaux des langages formels et des expressions régulières et oméga-régulières, en proposant des méthodes succinctes et formelles pour exprimer les langages réguliers et oméga-réguliers, respectivement.

Ce module vous plonge dans les principes essentiels des propriétés régulières et ω-régulières et comment elles sont représentées par des automates finis non déterministes (NFA) et des automates de Büchi (NBA), respectivement. Vous étudierez la notation et l'architecture des NFAs et NBAs, maîtriserez la construction d'expressions régulières et ω-régulières, et comprendrez leur corrélation avec ces automates. Le cours vous guidera à travers la conversion des NFAs en expressions régulières et des NBAs en expressions ω-régulières et l'inverse, en élucidant l'importance de ces concepts dans la vérification des comportements finis et infinis des systèmes.

Ce module propose une exploration approfondie des formules de logique temporelle linéaire (LTL), un formalisme mathématique permettant de décrire des langages contenant une infinité de mots. Il présente un cadre pour articuler les dimensions temporelles des comportements des systèmes, offrant une syntaxe qui reflète étroitement le langage naturel. En combinant la logique propositionnelle avec des opérateurs temporels, LTL fournit une boîte à outils puissante pour spécifier les comportements riches des systèmes