Dynamics: Dynamical and Arithmetical Model Checking

Membre de l'équipe :

• Valérie Berthe, directrice de recherche CNRS à l’Institut de recherche en informatique fondamentale (IRIF – CNRS/Université Paris Cité)
• Florian Luca, professeur à l’Université de Stellenbosch et membre du Max Planck Institute for Software Systems
• Joel Ouaknine, directeur de recherche au Max Planck Institute for Software Systems

Projet : Dynamical and Arithmetical Model Checking

DynAMiCs 
Les systèmes dynamiques discrets sont au cœur des principaux défis informatiques, de l’analyse des programmes et de la vérification assistée par ordinateur aux réseaux neuronaux et à la biologie théorique. Ces systèmes sont généralement simples à décrire, mais ils donnent lieu à une théorie algorithmique et mathématique qui regorge de problèmes ouverts. L’un de ces exemples est le célèbre problème de Skolem : l’orbite d’un système dynamique linéaire donné atteint-elle toujours un hyperplan donné ? La décidabilité de cette question est un problème ouvert de longue date, remontant à près d’un siècle !

L’objectif principal de DynAMiCs est de développer un cadre algorithmique pour formuler et répondre à des requêtes informatiques complexes sur les orbites de systèmes dynamiques géométriques. Bien que notre motivation et nos perspectives proviennent de l’informatique et de la vérification automatique, nous abordons ces problèmes sous des angles à la fois mathématiques et informatiques, en combinant des outils et des techniques de la théorie des nombres (approximation diophantienne, théorie de la transcendance, fractions continues), de la dynamique symbolique (combinatoire des mots, sous-décalages, systèmes de numération) et de la logique mathématique (logique monadique du second ordre, arithmétique de Presburger, théorie des automates). L’un de nos principaux objectifs est d’élargir considérablement le spectre des classes de systèmes dynamiques et des propriétés qui peuvent être traitées algorithmiquement par la vérification aidée par ordinateur.