Abstract FR:

Dans ce travail nous nous intéressons essentiellement aux trois points de vue importants adoptés dans la sémantique du parallélisme: l'étude d'équivalences comportementales compatibles avec le raffinement d'actions, les modèles dits de «vrai parallélisme», et les liens qui existent entre les logiques temporelles et les équivalences comportementales. Parmi les équivalences de bisimulation qui traitent les situations où certaines actions sont invisibles ou non observables de l'extérieur, la τ-bisimulation ou équivalence observationnelle de Milner et la η-bisimulation ne sont pas compatibles avec le raffinement d'actions. La bisimulation de branchement et la Δ-bisimulation sont compatibles avec le raffinement d'actions. Ceci nous a suggéré la recherche d'équivalences compatibles avec le raffinement et contenues dans la τ-bisimulation ou la η-bisimulation. Aussi, nous avons défini la notion de bisimulation avant arrière sur les structures d'événements primaires qui constituent un modèle de base pour le brai parallélisme. Nous avons généralisé cette nouvelle définition à la step, partial word et pomset bisimulation avant arrière. Nous avons comparé ces nouvelles équivalences aux autres équivalences de bisimulation sur les structures d'événements primaires. Il s'est avéré essentiellement que la pomset et la partial word bisimulations avant arrière coïncident avec la history preserving bisimulation. Partant de ce résultat, nous avons proposé une logique lbf, adéquate à la history preserving bisimulation. Nous avons aussi montré que la logique 1p de [DNF 90] caractérise elle aussi la history preserving bisimulation