Voir la source de PSPACE

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

==Définition formelle==

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

<math>\mbox{PSPACE} = \bigcup_{k\in\mathbb{N}} \mbox{SPACE}(n^k) \ . </math>

== Liens avec les autres classes ==
Le [[théorème de Savitch]]<ref>{{article  | nom = Savitch  | prénom = Walter  | titre = Relationships between nondeterministic and deterministic tape complexities  | journal =  Journal of Computer and System Sciences  | année = 1972  | numéro = 2  | volume = 4 }}</ref> 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 [[Adi Shamir|Shamir]] donne aussi, dans le contexte des [[système de preuve interactive|systèmes de preuve interactive]], que [[IP (complexité)|IP]] = PSPACE<ref>{{article|titre=IP = PSPACE|périodique=[[Journal of the ACM]]|volume=39|numéro=4|mois=octobre|année=1992|lire en ligne=http://portal.acm.org/citation.cfm?doid=146585.146609 IP = PSPACE|auteur=Adi Shamir|passage=869-877}}</ref>. 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<ref>{{Article|prénom1=Ashok K.|nom1=Chandra|prénom2=Dexter C.|nom2=Kozen|prénom3=Larry J.|nom3=Stockmeyer|titre=Alternation|périodique=J. ACM|volume=28|date=1981-01-01|issn=0004-5411|doi=10.1145/322234.322243|lire en ligne=http://doi.acm.org/10.1145/322234.322243|consulté le=2016-11-05|pages=114–133}}</ref>.

Comme l'illustre l'image ci-dessous, on a les inclusions suivantes : NL <math>\scriptstyle\subseteq</math> P <math>\scriptstyle\subseteq</math> [[NP (complexité)|NP]] <math>\scriptstyle\subseteq</math> PSPACE <math>\scriptstyle\subseteq</math> [[EXPTIME]] <math>\scriptstyle\subseteq</math> [[EXPSPACE]].
[[Image:Complexity subsets pspace.svg|200 px|center]]
D'après le théorème de hiérarchie en espace, [[NL (complexité)|NL]] et PSPACE sont différents. PSPACE contient la [[hiérarchie polynomiale]] : PH <math>\subseteq</math> 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 <math>Q_1x_1Q_2x_2...Q_nx_n\varphi(x_1,x_2,...,x_n)</math> où les <math>Q_i</math> sont des quantificateurs (<math>\forall</math> ou <math>\exists</math>) et les <math>x_i</math> sont des variables booléennes. Si une telle formule est [[Calcul des prédicats#Pr.C3.A9dicats.2C formules closes.2C formules polies.2C variables libres.2C variables li.C3.A9es|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 <math>\psi</math> ;
* Question : <math>\psi</math> 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<ref>
{{chapitre
 | nom = Hunt | prénom = H. B., III
 | titre chapitre = On the time and tape complexity of languages. I
 | titre ouvrage = Fifth Annual ACM Symposium on Theory of Computing (Austin, Tex., 1973)
 | passage = 10-19
 | lire en ligne = http://ecommons.cornell.edu/handle/1813/6007
 | année = 1973}}.</ref>. 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<ref>{{Article|langue=|auteur1=|prénom1=D.|nom1=Kozen|titre=Lower bounds for natural proof systems|périodique=18th Annual Symposium on Foundations of Computer Science (sfcs 1977)|date=1977-10|issn=|doi=10.1109/SFCS.1977.16|lire en ligne=https://ieeexplore.ieee.org/document/4567949/|consulté le=2019-07-08|pages=254–266|extrait=Def. 3.2.2 et Lemma 3.2.3, p. 261}}</ref>.

=== Planification ===
La [[Planification (intelligence artificielle)|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<ref>{{Article|langue=en|titre=The computational complexity of propositional STRIPS planning|périodique=Artificial Intelligence|volume=69|numéro=1-2|date=1994-09-01|issn=0004-3702|doi=10.1016/0004-3702(94)90081-7|lire en ligne=https://www.sciencedirect.com/science/article/pii/0004370294900817|consulté le=2018-02-28|pages=165–204}}</ref>.

=== 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 (jeu)|morpion]] ou de [[Othello (jeu)|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<ref>{{Computational Complexity (Arora et Barak)|numéro chapitre=4.2.2|titre chapitre=The essence of PSPACE: optimum strategies for game-playing}}.</ref>. La [[logique contrainte]] est un outil pour démontrer la PSPACE-difficulté de certains de ces jeux<ref>{{Article | langue=en |prénom1=Robert Aubrey|nom1=Hearn|titre=Games, puzzles, and computation| périodique=[[Massachusetts Institute of Technology]] (Thèse) | année=2016 |lire en ligne=http://dl.acm.org/citation.cfm?id=1269411|consulté le=2018-04-28}}</ref>.

=== Jeux dans les graphes ===
Le [[Géographie généralisée|jeu de géographie généralisé]] est PSPACE-complet<ref>{{Article|prénom1=Thomas J.|nom1=Schaefer|titre=On the complexity of some two-person perfect-information games|périodique=Journal of Computer and System Sciences|volume=16|numéro=2|date=1978-04-01|issn=0022-0000|doi=10.1016/0022-0000(78)90045-4|lire en ligne=http://www.sciencedirect.com/science/article/pii/0022000078900454|consulté le=2019-07-10|pages=185–225}}</ref>. Papadimitriou et Yannakakis ont défini des problèmes de [[Problème de plus court chemin|plus court chemin]] dans lequel l'agent ne possède pas entièrement la carte pour se déplacer ; ils sont PSPACE-complets<ref>{{Article|langue=en|prénom1=Christos H.|nom1=Papadimitriou|prénom2=Mihalis|nom2=Yannakakis|titre=Shortest paths without a map|périodique=Automata, Languages and Programming|série=Lecture Notes in Computer Science|éditeur=Springer Berlin Heidelberg|date=1989|isbn=9783540462019|doi=10.1007/bfb0035787|lire en ligne=https://link.springer.com/chapter/10.1007/BFb0035787|consulté le=2019-07-10|pages=610–620}}</ref>.

=== 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 :
* [[Calcul des propositions|logique propositionnelle]] [[Logique intuitionniste|intuitionniste]]{{Référence nécessaire|date=17 octobre 2016}} ;
* [[logique modale]] K<ref name=":0">{{Ouvrage|langue=anglais|auteur1=[[Richard E. Ladner]]|titre=The computational complexity of provability in systems of modal propositional logic|passage=467--480|lieu=|éditeur=SIAM journal on computing|année=1977|pages totales=|isbn=|lire en ligne=http://www.cs.man.ac.uk/~ezolin/ml/bib/Computational_complexity_of_provability_in_systems_of_modal_logic_(SIAMJC_1977).pdf}}.</ref>, logique modale S4<ref name=":0" /> ;
* théorie de l'égalité du [[Calcul des prédicats|premier ordre]]{{Référence nécessaire|date=17 octobre 2016}} ;
* [[Logique temporelle linéaire|LTL]] (''{{Langue|en|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érence nécessaire|date=17 octobre 2016}}.

== Autres problèmes dans PSPACE ==
En 1999, W. Plandowski a démontré que la satisfaisabilité d'une équation de mots est dans PSPACE<ref>{{Article|prénom1=Wojciech|nom1=Plandowski|titre=Satisfiability of Word Equations with Constants is in PSPACE|périodique=Proceedings of the 40th Annual Symposium on Foundations of Computer Science|série=FOCS '99|éditeur=IEEE Computer Society|date=1999|isbn=9780769504094|lire en ligne=http://dl.acm.org/citation.cfm?id=795665.796529|consulté le=2019-06-24|pages=495–}}</ref>, alors que l'on ne connaissait qu'une [[Borne supérieure et borne inférieure|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<ref>{{Article|prénom1=John|nom1=Canny|titre=Some Algebraic and Geometric Computations in PSPACE|périodique=Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing|série=STOC '88|éditeur=ACM|date=1988|isbn=9780897912648|doi=10.1145/62212.62257|lire en ligne=http://doi.acm.org/10.1145/62212.62257|consulté le=2019-06-24|pages=460–467}}</ref>.

==Bibliographie==
* {{Computational Complexity (Arora et Barak)}}

==Liens externes==
* {{Complexity Zoo|fin=P#pspace|nom=PSPACE}}

==Notes et références==
<references />

{{Palette|Théorie de la complexité}}

{{Portail|Informatique théorique}}

[[Catégorie:Classe de complexité]]