Vers une vérification automatique des systèmes dynamiques discrets

On pourrait les croire réservées à l’astrophysique, mais les questions d’orbite taraudent aussi l’informatique. Valérie Berthé, directrice de recherche CNRS à l’Institut de recherche en informatique fondamentale (IRIF - CNRS/Université Paris Cité), est en effet experte dans l’étude des orbites des systèmes dynamiques discrets. Un système dynamique est un système dont l’évolution dans le temps est régie par une loi. Il est de plus dit discret si son évolution se fait à des moments précis et avec une cadence fixe. Ces objets presque universels se retrouvent entre autres dans l’analyse des programmes, la vérification assistée par ordinateur, les réseaux neuronaux et même en biologie théorique.

« On utilise des systèmes dynamiques discrets dès que l’on itère une transformation, par exemple lors de l’étude d’une boucle dans un programme, explique Valérie Berthé. À force d’opérer des itérations sur un espace, on forme des orbites, des trajectoires, dont on veut étudier les propriétés, comme savoir combien de temps une orbite passe dans une région donnée de l’espace. On peut également considérer des propriétés de décision et d’atteignabilité autour de ces trajectoires : par exemple savoir si, étant donné une condition initiale, une trajectoire va atteindre un point ou une zone donnée. »

En informatique, cela peut par exemple servir à décider si l’exécution d’une boucle dans un programme doit s’arrêter ou se poursuivre, en fonction de conditions choisies. On retrouve aussi les systèmes dynamiques discrets dans le cadre de la vérification de modèles, où ils interviennent pour vérifier si un système modélisé satisfait bien, de façon certifiée, les conditions souhaitées, exprimées par exemple sous la forme d’expressions logiques.

Le projet DynAMiCs, pour Dynamical and arithmetical model checking, vise à pouvoir traiter algorithmiquement les systèmes dynamiques discrets, afin qu’ils puissent bénéficier des outils de vérification automatique assistée par ordinateur. Soutenu par une bourse européenne ERC Synergy, DynAMiCs est piloté par Valérie Berthé, mais également par Florian Luca, professeur à l’Université de Stellenbosch en Afrique du Sud, spécialiste de la théorie des nombres et membre du Max Planck Institute for Software Systems en Allemagne, et Joël Ouaknine, directeur de recherche au même institut et expert en vérification de modèles. Ils ont déjà commencé à publier ensemble en amont du projet, ce qui leur a permis de mieux comprendre les outils et méthodes de chacun.

Des compétences qui ne seront pas de trop pour lever les multiples obstacles qui attendent les chercheurs. Valérie Berthé cite en particulier le problème de Skolem. Ouvert depuis près d’un siècle, ce problème fait que l’on ne peut pas décider si l’orbite d’un système dynamique linéaire atteint toujours un hyperplan donné. Il n’a été résolu que pour quelques cas particuliers, en dehors desquels il demeure réfractaire à un véritable traitement algorithmique.

Pour le résoudre dans les cas les plus utiles, les chercheurs vont faire appel à des outils tels que la théorie des nombres, la dynamique symbolique et la logique mathématique. Ils élargiront ainsi au maximum les types de systèmes dynamiques discrets, ainsi que leurs propriétés, qui peuvent être manipulés par des algorithmes de vérification assistée par ordinateur.

« Le traitement algorithmique des systèmes dynamiques discrets présente de forts liens avec le domaine des automates et de la logique, ainsi qu’avec la théorie des nombres, ajoute Valérie Berthé. Nous voulons, entre autres, comprendre comment appliquer et combiner certaines techniques issues de la théorie des automates et de la théorie de la transcendance aux systèmes dynamiques discrets, puis aider ces trois mondes à communiquer en établissant un dictionnaire adéquat ». Les scientifiques devraient alors avoir réuni suffisamment d’outils pour lever les verrous de la vérification des systèmes dynamiques discrets.