Contributions à la sémantique du parallélisme : bisimulations pour le raffinement et le vrai parallélisme / Ferroudja Cherief ; sous la direction de [Philippe Jorrand]

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Parallélisme (informatique)

Sifakis, Joseph (1946-.... ; informaticien) (Membre du jury / opponent)

Jorrand, Philippe (19..-.... ; informaticien) (Directeur de thèse / thesis advisor)

Institut national polytechnique (Grenoble ; 1900-....) (Organisme de soutenance / degree-grantor)

Laboratoire d'informatique fondamentale et d'intelligence artificielle (Grenoble ; 19..-2007) (Laboratoire associé à la thèse / thesis associated laboratory)

Relation : Contributions à la sémantique du parallélisme : bisimulations pour le raffinement et le vrai parallélisme / Ferroudja Cherief ; sous la direction de [Philippe Jorrand] / Grenoble : Université Joseph Fourier , 2008

Relation : Contributions à la sémantique du parallélisme : bisimulations pour le raffinement et le vrai parallélisme / Ferroudja Cherief ; sous la direction de [Philippe Jorrand] / Grenoble : Atelier national de reproduction des thèses , 1992

Résumé / Abstract : 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