Décider (ℝ,+,<,1) dans (ℝ,+,<,ℤ)

February 24, 2020

Alexis Bes (LACL - UPEC)

La structure (R,+,<,Z), où R désigne l'ensemble des réels et Z le prédicat unaire "être un entier", admet l'élimination des quantificateurs et est décidable. Elle intervient notamment dans le domaine de la spécification et la vérification de systèmes hybrides. Elle peut être étudiée via les automates, en considérant des automates de Büchi qui lisent des réels représentés dans une base entière fixée. Boigelot et al. ont démontré en particulier que la classe des relations définissables dans (R,+,<,Z) coïncide avec celle des relations reconnaissables par automate en toute base. Une autre structure intéressante est (R,+,<,1), qui est moins expressive que (R,+,<,Z) mais définit les mêmes relations bornées. On présente une caractérisation topologique des relations définissables dans (R,+,<,Z) qui sont définissables dans (R,+,<,1), et on en déduit que le problème de savoir si une relation définissable dans (R,+,<,Z) est définissable dans (R,+,<,1) est décidable.
Travail en commun avec Christian Choffrut.