Sur les invariants de boucles pour les "programmes en temps continu"

Un système dynamique peut-être considéré comme un programme informatique en temps continu. Les concepts et objets classiques d'un programme, utiles notamment pour la vérification formelle (comme les invariants de boucles), ont leurs homologues, connus ou à définir, en temps continu. Densifier le temps demande néanmoins une certaine prudence et, surtout, une boite à outils adaptée à la tâche. Par exemple, l'opérateur successeur sur les entiers est bien défini et est même un concept de base dans l'arithmétique de Peano. C'est quoi "le" réel qui succède immédiatement un réel donné ? D'ailleurs, peut-on parler de principe d'induction sur les réels ? Je donnerai certains éléments de réponses à ces questions en m'attardant sur les problèmes de décidabilité et calculabilité d'invariants linéaires et algébriques.