PSPACE

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

Si l'on appelle ${\mbox{SPACE}}(t(n))$ l'ensemble des problèmes de décision décidés par des machines de Turing déterministes utilisant un espace $O(t(n))$ pour une fonction $t$ en la taille de l'entrée $n$ , alors on définit PSPACE formellement par :

${\mbox{PSPACE}}=\bigcup _{k\in \mathbb {N} }{\mbox{SPACE}}(n^{k})\ .$

Liens avec les autres classes

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 $\scriptstyle \subseteq$ P $\scriptstyle \subseteq$ NP $\scriptstyle \subseteq$ PSPACE $\scriptstyle \subseteq$ EXPTIME $\scriptstyle \subseteq$ EXPSPACE.

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 $\subseteq$ PSPACE.

Problèmes PSPACE-complets

À 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

Une formule booléenne quantifiée (abrégé QBF pour Quantified Boolean Formula) est une formule de la forme $Q_{1}x_{1}Q_{2}x_{2}...Q_{n}x_{n}\varphi (x_{1},x_{2},...,x_{n})$ où les $Q_{i}$ sont des quantificateurs ( $\forall$ ou $\exists$ ) et les $x_{i}$ 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 $\psi$ ;
Question : $\psi$ est-elle vraie ?

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

Théorie des langages

É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

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

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

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

À 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 ;
logique modale K[11], logique modale S4[11] ;
théorie de l'égalité du premier ordre ;
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.

Autres problèmes dans PSPACE

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

(en) Sanjeev Arora et Boaz Barak, Computational Complexity : A Modern Approach, Cambridge University Press, 2009 (ISBN 0-521-42426-7)

Liens externes

(en) La classe PSPACE sur le Complexity Zoo

Notes et références

Walter Savitch, « Relationships between nondeterministic and deterministic tape complexities », Journal of Computer and System Sciences, vol. 4, n^o 2,‎ 1972
Adi Shamir, « IP = PSPACE », Journal of the ACM, vol. 39, n^o 4,‎ octobre 1992, p. 869-877 (lire en ligne)
Ashok K. Chandra, Dexter C. Kozen et Larry J. Stockmeyer, « Alternation », J. ACM, vol. 28,‎ 1^er janvier 1981, p. 114–133 (ISSN 0004-5411, DOI 10.1145/322234.322243, lire en ligne, consulté le 5 novembre 2016)
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), 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),‎ octobre 1977, p. 254–266 (DOI 10.1109/SFCS.1977.16, lire en ligne, consulté le 8 juillet 2019) :
« Def. 3.2.2 et Lemma 3.2.3, p. 261 »
(en) « The computational complexity of propositional STRIPS planning », Artificial Intelligence, vol. 69, n^os 1-2,‎ 1^er septembre 1994, p. 165–204 (ISSN 0004-3702, DOI 10.1016/0004-3702(94)90081-7, lire en ligne, consulté le 28 février 2018)
(en) Sanjeev Arora et Boaz Barak, Computational Complexity : A Modern Approach, Cambridge University Press, 2009 (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),‎ 2016 (lire en ligne, consulté le 28 avril 2018)
Thomas J. Schaefer, « On the complexity of some two-person perfect-information games », Journal of Computer and System Sciences, vol. 16, n^o 2,‎ 1^er avril 1978, p. 185–225 (ISSN 0022-0000, DOI 10.1016/0022-0000(78)90045-4, lire en ligne, consulté le 10 juillet 2019)
(en) Christos H. Papadimitriou et Mihalis Yannakakis, « Shortest paths without a map », Automata, Languages and Programming, Springer Berlin Heidelberg, lecture Notes in Computer Science,‎ 1989, p. 610–620 (ISBN 9783540462019, DOI 10.1007/bfb0035787, lire en ligne, consulté le 10 juillet 2019)
(en) Richard E. Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM journal on computing, 1977 (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,‎ 1999, p. 495– (ISBN 9780769504094, lire en ligne, consulté le 24 juin 2019)
John Canny, « Some Algebraic and Geometric Computations in PSPACE », Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, ACM, sTOC '88,‎ 1988, p. 460–467 (ISBN 9780897912648, DOI 10.1145/62212.62257, lire en ligne, consulté le 24 juin 2019)

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.