Les lundis, à partir de 14h - UPEC CMC - Salle P2-131

23 mars 2020

TBA

Barnaby Martin (Durham)

TBA

16 mars 2020

TBA

Philipp Schlicht (University of Bristol)

TBA

9 mars 2020

TBA

Jean Marie Madiot (INRIA Paris)

TBA

3 mars 2020

TBA

David Auger (Université de Versailles)

24 février 2020

Décider (R,+,<,1) dans (R,+,<,Z)

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.