Invariance et contrôle symbolique pour les systèmes monotones, application aux bâtiments intelligents

English

Séminaire Modèles et Algorithmes Déterministes: CASYS

15/05/2014 - 09:45 Mr Jean-Guillaume Dumas Salle 1 - Tour IRMA

Un certificat en algèbre linéaire est une structure de donnée ajoutée au résultat d'un calcul qui permet à un algorithme de vérification, potentiellement probabiliste, de prouver la validité du résultat. Cela permet par exemple d'externaliser des calculs à un "cloud" et de vérifier a posteriori que les calculs ont bien été effectués, mais à un coût inférieur à celui du calcul lui-même.

Nous donnons dans cet exposé deux types de certificats interactifs :
d'abord des certificats essentiellement optimaux pour la forme normale de Frobenius, les polynômes minimaux et caractéristiques, et le caractère défini de matrices denses à coefficients entiers ;
ensuite des certificats également essentiellement optimaux pour le calcul du rang de matrices creuses ou structurées. Par exemple, pour une matrice creuse, vérifier le rang est, à un facteur polylogarithmique près, dorénavant aussi rapide que de simplement énumérer tous les coefficients de la matrice.

Tous nos certificats utilisent des protocoles de vérification interactifs où l'interaction peut-être supprimée par une heuristique à la Fiat-Shamir. Dans ce cas la validité de la procédure de vérification est garantie par des hypothèses cryptographiques standard.