PSPACE

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

En informatique théorique, plus précisément en théorie de la complexité, PSPACE est la classe de complexité des problèmes de décision décidés par une machine de Turing déterministe avec un espace polynomial.

Définition formelle[modifier | modifier le code]

Si l'on appelle l'ensemble des problèmes de décision décidés par des machines de Turing déterministes utilisant un espace pour une fonction en la taille de l'entrée , alors on définit PSPACE formellement par :

Liens avec les autres classes[modifier | modifier le code]

Le théorème de Savitch[1] indique que PSPACE=NPSPACE, c'est-à-dire qu'en espace polynomial, les machines déterministes et non déterministes ont la même expressivité. Par le théorème d'Immerman-Szelepcsényi, PSPACE=coNPSPACE. Le théorème de Shamir donne aussi, dans le contexte des systèmes de preuve interactive, que IP = PSPACE[2]. La classe PSPACE est égale à AP, la classe des problèmes de décision décidés par une machine de Turing alternante en temps polynomial[3].

Comme l'illustre l'image ci-dessous, on a les inclusions suivantes : NL P NP PSPACE EXPTIME EXPSPACE.

Complexity subsets pspace.svg

D'après le théorème de hiérarchie en espace, NL et PSPACE sont différents. PSPACE contient la hiérarchie polynomiale : PH PSPACE.

Problèmes PSPACE-complets[modifier | modifier le code]

À l'instar de la NP-complétude, on peut définir la notion de problèmes PSPACE-complets. Un problème est PSPACE-dur si tout problème dans PSPACE s'y réduit en temps polynomial. Un problème est PSPACE-complet s'il est dans PSPACE et il est PSPACE-dur.

Formules booléennes quantifiées[modifier | modifier le code]

Une formule booléenne quantifiée (abrégé QBF pour Quantified Boolean Formula) est une formule de la forme où les sont des quantificateurs ( ou ) et les sont des variables booléennes. Si une telle formule est close, alors elle est vraie ou fausse.

Le problème QBF-SAT (satisfiabilité d'une formule booléenne quantifiée), aussi appelé TQBF (pour true quantified Boolean formula) est :

  • Entrée : une formule QBF close  ;
  • Question : est-elle vraie ?

Le problème QBF-SAT est PSPACE-complet.

Universalité des langages réguliers[modifier | modifier le code]

Étant donné une expression rationnelle, le problème qui consiste à savoir si elle génère tous les mots possibles est PSPACE-complet[4].

Planification[modifier | modifier le code]

La planification classique, où il s'agit de savoir s'il existe une suite d'actions pour atteindre un but depuis une situation initiale (situation initiale, but et actions décrites dans un langage succinct comme STRIPS) est PSPACE-complet[5].

Jeux[modifier | modifier le code]

Pour certains jeux, savoir si l'un des joueurs a une stratégie gagnante depuis une certaine situation du jeu, est PSPACE-complet. Par exemple certaines versions de hex, du morpion ou de Othello ont cette propriété. De façon plus générale, certains auteurs considèrent qu'un des concepts centraux de PSPACE est le fait de pouvoir définir une stratégie optimale pour les jeux à deux joueurs avec information parfaite[6]. La logique contrainte est un outil pour démontrer la PSPACE-dureté de certains de ces jeux[7].

Logique[modifier | modifier le code]

À l'instar du problème de satisfiabilité d'une formule booléenne quantifiée (voir plus haut), les problèmes de satisfiabilité des logiques suivantes sont PSPACE-complets :

La vérification de modèles d'une propriété des logiques suivantes est PSPACE-complète :

Autres problèmes dans PSPACE[modifier | modifier le code]

En 1999, W. Plandowski a démontré que la satisfiabilité d'une équation de mots est dans PSPACE[9], alors que l'on ne connaissait qu'une borne supérieure dans NEXPTIME. Le problème de satisfiabilité d'une formule du premier ordre quantifiée existentiellement dans la théorie des réels est dans PSPACE[10].

Bibliographie[modifier | modifier le code]

Liens externes[modifier | modifier le code]

Notes et références[modifier | modifier le code]

  1. Walter Savitch, « Relationships between nondeterministic and deterministic tape complexities », Journal of Computer and System Sciences, vol. 4, no 2,‎
  2. Adi Shamir, « IP = PSPACE », Journal of the ACM, vol. 39, no 4,‎ , p. 869-877 (lire en ligne)
  3. Ashok K. Chandra, Dexter C. Kozen et Larry J. Stockmeyer, « Alternation », J. ACM, vol. 28,‎ , p. 114–133 (ISSN 0004-5411, DOI 10.1145/322234.322243, lire en ligne, consulté le 5 novembre 2016)
  4. H. B., III Hunt, « On the time and tape complexity of languages. I », dans Fifth Annual ACM Symposium on Theory of Computing (Austin, Tex., 1973), (lire en ligne), p. 10-19.
  5. (en) « The computational complexity of propositional STRIPS planning », Artificial Intelligence, vol. 69, nos 1-2,‎ , p. 165–204 (ISSN 0004-3702, DOI 10.1016/0004-3702(94)90081-7, lire en ligne, consulté le 28 février 2018)
  6. (en) Sanjeev Arora et Boaz Barak, Computational Complexity : A Modern Approach, Cambridge University Press, (ISBN 0-521-42426-7), chap. 4.2.2 (« The essence of PSPACE: optimum strategies for game-playing »).
  7. (en) Robert Aubrey Hearn, « Games, puzzles, and computation », Massachusetts Institute of Technology (Thèse),‎ (lire en ligne, consulté le 28 avril 2018)
  8. a et b (en) Richard E. Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM journal on computing, (lire en ligne), p. 467--480.
  9. Wojciech Plandowski, « Satisfiability of Word Equations with Constants is in PSPACE », Proceedings of the 40th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, série FOCS '99,‎ , p. 495– (ISBN 9780769504094, lire en ligne, consulté le 24 juin 2019)
  10. John Canny, « Some Algebraic and Geometric Computations in PSPACE », Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, ACM, série STOC '88,‎ , p. 460–467 (ISBN 9780897912648, DOI 10.1145/62212.62257, lire en ligne, consulté le 24 juin 2019)