Abstract FR:

Les executions d'applications reparties exhibent une structure d'ordre partiel et les recherches actuelles se portent d'une part, sur la representation efficace de cet ordre partiel, d'autre part sur la verification de proprietes du systeme observe. Ainsi il est souhaite de disposer d'un codage necessitant une memoire minimale, un temps minimal de pre-traitement des donnees et une reponse rapide et exacte a la question l'evenement x precede-t-il l'evenement y ? un codage qui se conformerait a ces criteres serait exact et optimal. L'exactitude d'un codage suppose qu'il puisse caracteriser les relations de causalite mais aussi la concurrence entre evenements ; en theorie, cette exactitude est conditionnee par la connaissance de la dimension et largeur de l'ordre partiel. Mais en pratique, les contraintes incontournables de calcul a la volee rendent peu aisee l'obtention de ces valeurs. L'exploration des differentes methodes laisse apparaitre qu'il est difficile de concevoir un codage a usage general ; au contraire, il apparait que l'identification de classes d'ordre exhibant des proprietes qui permettent une representation efficace est une direction d'investigation prometteuse. A partir d'une representation des chaines de l'ordre partiel, le probleme de l'optimalite du codage a ete aborde par le biais de decompositions de l'ensemble partiellement ordonne. Ces decompositions visent a minimiser le nombre de paires d'elements, ordonnes au sein des decompositions, mais incomparables au sein de l'ordre partiel. Ce type de decompositions fournit des approximations d'un codage optimal, en se rapprochant de la largeur, dans le cas general ; l'optimalite est atteinte dans des cas specifiques. Independamment de la representation choisie, la verification de proprietes reste une tache couteuse ; une propriete doit etre en effet verifiee sur l'ensemble des observations possibles. Par le biais des decompositions, les proprietes sont verifiees sur un sous-ensemble significatif des observations, constitue par l'ensemble des extensions lineaires optimales. Dans cette optique, le cout de la verification de proprietes est moindre