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 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. 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.

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. 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.

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.

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. La logique contrainte est un outil pour démontrer la PSPACE-difficulté de certains de ces jeux.

Jeux dans les graphes

Le jeu de géographie généralisé est PSPACE-complet. 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.

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^{[réf. nécessaire]} ;
• logique modale K, logique modale S4 ;
• 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

En 1999, W. Plandowski a démontré que la satisfaisabilité d'une équation de mots est dans PSPACE, 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.

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