Structure automatique

En informatique théorique, une structure automatique[1] est une structure définie à partir d'automates finis. L'intérêt principal de ces structures est de représenter de manière finie des objets infinis, ce qui offre un cadre « naturel » à la décidabilité de problèmes.

En particulier, la vérification de modèles de formules de la logique du premier ordre est décidable sur les structures automatiques.

IntroductionModifier

StructuresModifier

On considère des structures de la forme  où :

  •   est un ensemble (dénombrable) ;
  •   sont des prédicats sur   d'arités   ;
  •   sont des fonctions (partielles) sur   d'arités  .

Quitte à remplacer les fonctions des prédicats caractérisant leurs graphes, on peut supposer que les structures sont purement relationnelles.

Structures récursivesModifier

Il semble naturel qu'afin de décider des propriétés logiques sur une structure, celle-ci doive posséder une représentation finie.

C'est l'idée que généralisent les structures récursives[2] : l'ensemble de leurs éléments   est récursif, et les ensembles de r-uplets définis par les relations le sont également. On peut donc représenter de telles structures par une collection finie de machines de Turing.

Néanmoins les nombreux résultats d'indécidabilité[2] sur ces structures très générales montrent qu'il est nécessaire de se restreindre à certaines sous-classes, comme les structures automatiques.

Définition formelleModifier

Structures automatiquesModifier

Une structure relationnelle  est dite automatique s'il existe un alphabet fini  , un langage   et une fonction de décodage surjective   tels que :

  •  , le domaine de  , est un langage régulier de  ;
  •  (qui caractérise les défauts d'injectivité) est reconnu par un transducteur synchrone (sans  -règles) ;
  • Pour tout prédicat   d'arité  , le langage  est reconnu par un transducteur synchrone.

Représentations automatiquesModifier

Toute structure automatique   possède une représentation automatique sous la forme  où :

  •   est un automate fini sur   qui reconnaît   ;
  •   est un transducteur synchrone qui reconnaît   ;
  • Chaque   est un transducteur synchrone qui reconnaît  .

C'est à partir de cette représentation que l'on va décider certaines propriétés de la structure.

ExemplesModifier

  1. Les structures finies sont automatiques.
  2. L'ensemble des entiers naturels muni de l'addition   est automatique. On code les entiers en base 2 avec le bit de poids fort à droite et l'addition est représentée avec un transducteur synchrone.
  3. On peut étendre la structure précédente avec une relation de divisibilité restreinte :   si   est une puissance de   qui divise  . Pour tout  , la structure   est automatique.
  4. Les groupes automatiques sont des cas particuliers de structures automatiques qui sont des groupes.

Représentation automatique de  Modifier

 
Automate qui vérifie l'addition. Il accepte un mot   si le nombre   est égal à la somme de  et  .

Le langage   est l'ensemble des mots finis sur l'alphabet {0, 1}. La fonction de décodage associe à tout mot fini m l'entier dont la représentation binaire avec le bit de poids fort à droite est m. Par exemple, le mot 00101 se décode en 4+8 = 12. L'addition est représentée par l'automate à deux états donnée dans la figure de droite.

Décidabilité de la vérification de modèlesModifier

Étant donnée une représentation d'une structure automatique, la vérification de modèles d'une formule logique du premier ordre sur le langage des prédicats de la structure est décidable.

En particulier, étant donnée une formule   de variables libres   sur ce langage, il est possible de construire un transducteur synchrone reconnaissant l'ensemble des codages d'éléments vérifiant la formule : .

Il est possible d'étendre la logique du premier ordre avec un quantificateur  dont la sémantique est définie comme « il existe une infinité ». Grâce au lemme de l'étoile, on peut montrer que la vérification de modèles de cette logique étendue reste décidable sur les structures automatiques.

Propriétés remarquablesModifier

Injectivité de la représentationModifier

À partir d'une représentation automatique d'une structure, il est possible d'en construire une représentation injective.

Une telle représentation vérifie que la fonction de décodage   est injective, ou de manière équivalente, que  .

ClôtureModifier

La classe des structures automatiques est closes par :

  • mise à une puissance finie ;
  • quotient par une relation définissable au premier ordre ;
  • ajout d'un prédicat définissable au premier ordre ;
  • restriction à une sous-structure dont le domaine est définissable au premier ordre.

ExtensionsModifier

Par définition, les structures automatiques sont finies ou dénombrables. Il est possible d'étendre la définition à des ensembles ayant la puissance du continu via un encodage par des mots infinis, on parle alors de structure  -automatique.

Notes et référencesModifier

  1. Achim Blumensath et Erich Grädel, « Automatic Structures », Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, série LICS '00,‎ , p. 51– (ISBN 0769507255, lire en ligne, consulté le 11 juin 2016).
  2. a et b (en) T. Hirst and D. Harel., « More about recursive structures: Descriptive complexity and zero-one laws », Proc. 11th IEEE Symp. on Logic in Computer Science,‎ , p. 334-348 (lire en ligne).