PSPACE — Wikipédia
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.
![](http://upload.wikimedia.org/wikipedia/commons/thumb/6/6e/Complexity_subsets_pspace.svg/200px-Complexity_subsets_pspace.svg.png)
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-difficile 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-difficile.
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.
Théorie des langages
[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]. Il s'agit du problème d'universalité d'une expression rationnelle.
Savoir si l'intersection des langages de k automates finis déterministes est vide est aussi PSPACE-complet[5].
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[6].
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[7]. La logique contrainte est un outil pour démontrer la PSPACE-difficulté de certains de ces jeux[8].
Jeux dans les graphes
[modifier | modifier le code]Le jeu de géographie généralisé est PSPACE-complet[9]. Papadimitriou et Yannakakis ont défini des problèmes de plus court chemin dans lequel l'agent ne possède pas entièrement la carte pour se déplacer ; ils sont PSPACE-complets[10].
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 :
- logique propositionnelle intuitionniste[réf. nécessaire] ;
- logique modale K[11], logique modale S4[11] ;
- théorie de l'égalité du premier ordre[réf. nécessaire] ;
- LTL (linear-time logic : logique temporelle linéaire).
La vérification de modèles d'une propriété des logiques suivantes est PSPACE-complète :
- LTL ;
- CTL* ;
- logique du premier ordre[réf. nécessaire].
Autres problèmes dans PSPACE
[modifier | modifier le code]En 1999, W. Plandowski a démontré que la satisfaisabilité d'une équation de mots est dans PSPACE[12], 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[13].
Bibliographie
[modifier | modifier le code]- (en) Sanjeev Arora et Boaz Barak, Computational Complexity : A Modern Approach, Cambridge University Press, (ISBN 0-521-42426-7)
Liens externes
[modifier | modifier le code]Notes et références
[modifier | modifier le code]- Walter Savitch, « Relationships between nondeterministic and deterministic tape complexities », Journal of Computer and System Sciences, vol. 4, no 2,
- Adi Shamir, « IP = PSPACE », Journal of the ACM, vol. 39, no 4, , p. 869-877 (lire en ligne)
- 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 )
- 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.
- D. Kozen, « Lower bounds for natural proof systems », 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), , p. 254–266 (DOI 10.1109/SFCS.1977.16, lire en ligne, consulté le ) :
« Def. 3.2.2 et Lemma 3.2.3, p. 261 »
- (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 )
- (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 »).
- (en) Robert Aubrey Hearn, « Games, puzzles, and computation », Massachusetts Institute of Technology (Thèse), (lire en ligne, consulté le )
- Thomas J. Schaefer, « On the complexity of some two-person perfect-information games », Journal of Computer and System Sciences, vol. 16, no 2, , p. 185–225 (ISSN 0022-0000, DOI 10.1016/0022-0000(78)90045-4, lire en ligne, consulté le )
- (en) Christos H. Papadimitriou et Mihalis Yannakakis, « Shortest paths without a map », Automata, Languages and Programming, Springer Berlin Heidelberg, lecture Notes in Computer Science, , p. 610–620 (ISBN 9783540462019, DOI 10.1007/bfb0035787, lire en ligne, consulté le )
- (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.
- 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, fOCS '99, , p. 495– (ISBN 9780769504094, lire en ligne, consulté le )
- John Canny, « Some Algebraic and Geometric Computations in PSPACE », Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, ACM, sTOC '88, , p. 460–467 (ISBN 9780897912648, DOI 10.1145/62212.62257, lire en ligne, consulté le )