Abstract FR:

Cette these s'inscrit dans le cadre de la verification des systemes infinis. Dans la premiere partie, nous nous interessons a la verification des schemas rpps, introduits par o. Kouchnarenko et ph. Schnoebelen. Nous proposons trois resultats : nous definissons rpa une nouvelle algebre de processus qui permet coder les schemas rpps de facon precise, nous montrons que l'atteignabilite entre des termes rpa est une relation reconnaissable et que l'accessibilite entre deux etats emboites rpps est un probleme np-complet. Dans la deuxieme partie, nous nous interessons a la decidabilite de l'equivalence de performance introduite par f. Corradini, r. Gorrieri et m. Roccetti pour un algebre obtenue a partir de l'algebre bpp en ajoutant du temps par l'intermediaire d'horloges locales. Notre resultat principal est que l'equivalence de performance est decidable pour cette algebre et qu'elle peut etre decidee en temps polynomial. De facon surprenante, l'ajout d'horloges locales ne rend pas le probleme plus complique (la bisimulation est un probleme co-np dur pour bpp).