EXPSPACE

classe de complexité

En théorie de la complexité, EXPSPACE est la classe des problèmes décidables en espace exponentiel par une machine de Turing déterministe.

Définition formelle modifier

Si l'on appelle   l'ensemble de tous les problèmes qui peuvent être résolus par des machines de Turing déterministes utilisant un espace   pour une fonction   en la taille de l'entrée  , alors on définit EXPSPACE par :

 

Liens avec les autres classes modifier

 
Diagramme d'inclusions de quelques classes de complexité. Les flèches indiquent l'inclusion.

Comme l'illustre l'image de droite, EXPSPACE contient la plupart des classes de complexité classiques. En particulier : NP   PSPACE   EXPTIME   EXPSPACE.

D'après le théorème de hiérarchie en espace (en), PSPACE est strictement incluse dans EXPSPACE. Savoir si EXPTIME est un sous-ensemble strict de EXPSPACE ou non est une question ouverte.

D'après le théorème de Savitch, EXPSPACE est égale à NEXPSPACE.

D'après le théorème d'Immerman-Szelepcsényi, EXPSPACE est égale à co-EXPSPACE.

EXPSPACE est incluse dans 2-EXPTIME (définie par  ).

Problèmes EXPSPACE-complets modifier

Un problème de décision est EXPSPACE-complet s'il est dans EXPSPACE et que tout problème de EXPSPACE s'y réduit en temps polynomial.

Problème de l'universalité d'un langage rationnel décrit par des expressions rationnelles avec exponentiation modifier

Un exemple de problème EXSPACE-complet consiste à déterminer si une expression rationnelle avec exponentiation génère l'ensemble des mots de l'alphabet sur lequel elle est définie[1],[2]. Si on ne dispose pas de l'exponentiation dans le langage des expressions rationnelles le problème devient PSPACE-complet. L'exponentiation permet d'exprimer certaines expressions de façon exponentiellement plus concise, et de passer de PSPACE-complet à EXPSPACE-complet. Ce résultat est démontré en détail ci-dessous.

Expression rationnelle avec exponentiation (REX) modifier

Les expressions rationnelles avec exponentiation (REX - Regular Expressions with Exponentiation) sur l'alphabet fini   sont les expressions obtenues à partir des lettres de A par les opérations suivantes :

  1. L'opération   ou   (représente l'union)
  2. L'opération   (représente le produit, le point est parfois omis)
  3. L'opération   (représente l'étoile de Kleene)
  4. L'opération   ou   (représente l'exponentiation d'ordre n)

À chaque REX   est associé un langage rationnel   défini inductivement par :

  1.  ,  
  2.    est une lettre de  
  3.  
  4.  
  5.   on note également   l'ensemble des mots possibles sur l'alphabet  
  6.  

On a par exemple :  . Il est possible de remplacer toute opération d'exponentiation d'ordre   par   concaténations (par exemple   est similaire à  ). Cependant, cette transformation peut accroître de façon exponentielle la taille de la formule. La concision de l'opération d'exponentiation participe à l'importante complexité spatiale du problème ci-dessous.

Langage des REX universelles modifier

À partir de la définition précédente d'une REX, on considère le langage suivant :

 

Le problème   consiste ainsi à déterminer si une REX   donnée génère l'ensemble des mots finis possibles sur son alphabet (une telle REX est qualifiée d'universelle). Ce problème est EXPSPACE-complet :

Théorème —  Le problème   est EXPSPACE-complet.

Ce théorème est toujours valable si on restreint l'exponentiation à l'ordre 2. Si l'étoile de Kleene est retirée, le problème devient NEXPTIME-complet.

Démonstration modifier

La démonstration du théorème précédant s'effectue en 2 étapes. Il faut tout d'abord prouver l'appartenance de   à EXPSPACE, puis montrer que ce langage est EXPSPACE-hard (autrement dit, tout langage de EXPSPACE se réduit en temps polynomial à  ).

  EXPSPACE

Étant donné une REX   de taille  , l'algorithme suivant permet de déterminer en espace exponentiel si   :

  1. Remplacer les opérations d'exponentiation par des concaténations. On obtient une formule de taille  .
  2. Convertir cette formule (de manière naïve) en un automate non déterministe. Cette opération nécessite un espace  .
  3. Déterminiser l'automate précédant. Le nouvel automate peut avoir jusqu'à   états.
  4.   appartient à   si et seulement si aucun état rejetant n'est atteignable dans l'automate déterministe précédant. D'après le théorème de Savitch, ceci se vérifie en espace   sur un graphe de taille  .

Puisqu'il n'est pas possible d'utiliser   espace, l'automate déterministe n'est pas construit à l'étape 3 ci-dessus. À la place, il est recalculé au fur et à mesure de son parcours lors de l'étape 4.

  est EXPSPACE-hard

Considérons un langage   reconnu par une machine de Turing déterministe   en espace  . On va associer à tout mot   une REX   telle que  . Plus précisément, on aura  .

L'état de la machine   au temps   de son exécution est représenté par le mot  , où   est le contenu de la case   du ruban,   l'état de la machine et   le symbole placé sous la tête de lecture. Puisque   s'exécute en espace  , on peut supposer que   est de taille   (quitte à compléter par des symboles blancs  ).

Un calcul de   sur une entrée   est alors représenté par le mot   où chaque   est l'encodage de l'état de la machine au temps   de son exécution.

Un calcul   de   sur une entrée   n'est pas rejetant s'il vérifie au moins une des 3 conditions suivantes :

  1.   n'est pas une configuration initiale possible de  .
  2. il existe 2 configurations successives   représentant une transition impossible.
  3.   n'est pas une configuration finale rejetante.

Pour chacune de ces 3 conditions, on construit une expression rationnelle   qui génère l'ensemble des mots vérifiant la condition (on note   et  ).

Condition 1. Au moment initial, la machine   est dans l'état   et   est écrit sur son ruban. Ainsi, la seule configuration initiale possible est :  . L'expression rationnelle suivante génère alors l'ensemble des mots vérifiant la condition 1 :  

Condition 2. Afin de savoir si une transition est valide ou non, il suffit d'étudier pour chaque paire de configurations successives des fenêtres de taille 3 centrées sur l'état courant (par exemple, pour la configuration   la fenêtre est  ). En effet, les autres lettres de la configuration ne sont pas censées évoluer après seulement un pas de calcul. Pour deux fenêtres   et   on note   s'il ne peut pas exister deux configurations successives ayant respectivement   et   pour fenêtres. On génère alors l'ensemble des mots vérifiant la condition 2 à l'aide de l'expression rationnelle suivante :  .

Condition 3. On suppose que la machine   finit dans l'état   en cas de calcul rejetant. Ainsi, pour que   ne soit pas une configuration finale rejetante, il suffit que   ne contienne pas  . L'expression rationnelle suivante génère ainsi l'ensemble des mots vérifiant la condition 3 :  .

Finalement, on note  . On a bien   et donc  . Par ailleurs,   se construit bien en temps polynomial en   (  est de taille  ).

En logique modifier

Le problème de satisfiabilité de certains fragments de la logique temporelle linéaire avec des quantifications du premier ordre est EXPSPACE-complet[3].

Problème d'accessibilité modifier

Le problème d'accessibilité dans les lossy VASS (vector addition systems with states) est EXPSPACE-complet[4].

Bibliographie modifier

Liens externes modifier

Notes et références modifier

  1. (en) Chris Umans, Kevin Lee, « Computational Complexity, Lecture Notes 8 »,
  2. Albert R. Meyer et Larry Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. 13th IEEE Symposium on Switching and Automata Theory, Oct 1972, pp.125–129.
  3. I. Hodkinson, R. Kontchakov, A. Kurucz et F. Wolter, « On the computational complexity of decidable fragments of first-order linear temporal logics », 10th International Symposium on Temporal Representation and Reasoning, 2003 and Fourth International Conference on Temporal Logic. Proceedings,‎ , p. 91–98 (DOI 10.1109/TIME.2003.1214884, lire en ligne, consulté le )
  4. (en) Charles Rackoff, « The covering and boundedness problems for vector addition systems », Theoretical Computer Science, vol. 6, no 2,‎ , p. 223–231 (ISSN 0304-3975, DOI 10.1016/0304-3975(78)90036-1, lire en ligne, consulté le )