Abstract FR:

Cette these traite de la specification logique des comportements de programmes. Les programmes etant modelises a l'aide de systemes de transitions, les comportements de programmes sont definis comme des classes d'equivalence de systemes de transitions, l'equivalence consideree etant l'equivalence de bisimulation de park. Dans ce cadre, une formule logique specifie une propriete de comportements lorsqu'elle admet une classe de modeles close par equivalence de bisimulation. Nous demontrons qu'une formule de la logique monadique du second ordre est comportementale au sens precedent si et seulement si elle est equivalente a une formule du mu-calcul modal de kozen. Ce resultat donne un sens precis a l'assertion la plupart des logiques de programmes peuvent etre traduites en mu-calcul modal. Techniquement, notre approche developpe la theorie des automates sur les arbres finis ou infinis, mettant en evidence le role unificateur que jouent les calculs de points-fixes vis a vis de la theorie des modeles d'une part et de la theorie des automates d'autre part