Cette thèse étudie l’atteignabilité de problèmes de contrôle linéaires soumis à des contraintes bornées sur le contrôle. En utilisant une approche basée sur de l’analyse convexe et des hyperplans supports, nous introduisons une fonctionnelle J dont la positivité sur l’espace d’état est équivalente à l’atteignabilité de l’ensemble cible. Cette fonctionnelle a l’avantage de dépendre uniquement des contraintes sur le contrôle et de la solution du problème adjoint.

À l’aide de cette fonctionnelle, nous nous concentrons sur les preuves de non-atteignabilité — celle-ci étant équivalente à trouver un point où J est négative. Nous introduisons une méthode assistée par ordinateur basée sur la discrétisation puis la minimisation de J. Dans un premier temps, nous minimisons une version discrétisée J_d de J, dans le but de trouver un point négatif. Ensuite, nous majorons les erreurs de discrétisation grâce à de nouvelles bornes explicites, et bornons les erreurs d’arrondis en utilisant de l’arithmétique d’intervalles. Finalement, la valeur de la fonctionnelle originelle J est incluse dans un intervalle explicite, dont la stricte négativité fournit une preuve assistée par ordinateur de non-atteignabilité de la cible choisie.

Nous démontrons l’efficacité de la méthode tant en dimension finie qu’infinie : tout d’abord, nous la formalisons dans le cadre de systèmes de dimension finie et développons des majorations explicites d’erreurs de discrétisation. Ces résultats sont appliqués à de nombreux exemples, fournissant des preuves de non-atteignabilité ainsi que des minorations de temps minimaux d’atteignabilité. Dans un second temps, nous étendons la méthode à des systèmes de contrôle paraboliques, avec l’équation de la chaleur en une dimension comme exemple type. En majorant finement les erreurs de discrétisation, nous obtenons des preuves de non-atteignabilité sous des contraintes réalistes.

La fonctionnelle J peut également être utilisée pour prouver des résultats positifs d’atteignabilité : cette thèse présente ainsi des travaux en cours sur des preuves assistées par ordinateur d’approximations tant intérieures qu’extérieures de l’ensemble atteignable.