Vérification Approchée et Complexité : 2012-2013

Michel de Rougemont, Liafa et Université Paris II

La vérification consiste à décider si une structure satisfait une propriété. On peut proposer une preuve classique, qui peut cependant être très longue, en particulier pour une propriété qui n’est pas dans la classe NP. On cherche alors à savoir s’il est possible de montrer à l’aide d’une preuve courte qu’une propriété soit vraie avec grande probabilité. C’est le rôle des preuves interactives et des preuves vérifiables avec grande probabilité qui correspondent aux classes de complexité IP et PCP.

Si on cherche des preuves très rapides, on peut introduire une approximation ε et décider si la structure satisfait la propriété ou si elle est ε-loin de la satisfaire, en utilisant une distance entre structures. Si la structure de taille n est très grande, on peut souhaiter des preuves en temps indépendant de n et dépendant uniquement de ε ou peut-être des preuves en temps log n. On parle alors de Test de propriété. Les applications classiques de ces concepts sont :

• Des preuves interactives pour des problèmes coNP et PESPACE
• Des preuves PCP avec un nombre constant de requêtes pour des problèmes NP,
• Des preuves approchées pour des problèmes NP durs ou PESPACE durs

Les applications informatiques sont :

• Le Model Checking approché,
• Des décisions approchées pour les masses de données,
• Des décisions approchées sur des données de flux (Streaming).

PROGRAMME

1. Rappels sur les classes RP et BPP
2. Preuves interactives, IP : preuve du permanent et de QBF.
3. PCP(r(n),q(n)) : exemples
4. Le théorème PCP
5. Le test de propriétés : graphes, mots, arbres,
6. Les algorithmes de Streaming et la Complexité en Communication

BIBLIOGRAPHIE

[1] Computational Complexity: A Modern Approach, Sanjeev Arora et Boaz Barak, Cambridge University Press 2009,

[2]. The PCP theorem by gap amplification, Irit Dinur, Journal of the ACM 54 (3): 12, 2007.

[3] Logic and Complexity, R. Lassaigne and M. de Rougemont, Springer 2004.

Référence IP protocoles sur les graphes: FSTTCS paper

Référence Test de linéarité via Analyse de Fourier: Notes sur le test de linéarité

Test de propriété: Tests basés sur les statistiques

Test de propriété avec ustat: Notes du cours

Algorithmes de Streaming: Streaming

Algorithmes de Streaming 2: Streaming 2

Algorithmes Bellagio: Bellagio