14/12/2000: Paul Gastin (LIAFA)
Utilisation des traces pour une sémantique dénotationnelle

Résumé
Le plus souvent, dans les sémantiques opérationnelles et dénotationnelles des algèbres de processus, le parallélisme est représenté par le choix non déterministe. Ceci provient du fait que le modèle sémantique utilisé est séquentiel. Nous souhaitons montrer que l'on peut faire la différence entre parallélisme et choix non déterministe en utilisant des modèles basés sur les ordres partiels étiquetés (pomsets), comme les traces de Mazurkiewicz et leurs généralisations.
Pour illustrer ceci, on propose une algèbre de processus élémentaire comportant une composition (faiblement) séquentielle, une composition parallèle, un opérateur de restriction, un opérateur de masquage et qui permet les constructions récursives. Nous avons délibérément exclu les opérateurs de choix de ce langage.
On développe une sémantique opérationnelle et une sémantique dénotationnelle pour ce langage et on prouve un théorème de congruence qui relie les comportements opérationnels d'un processus et sa description dénotationnelle. En particulier, on obtient l'adéquation entre la sémantique opérationnelle et la sémantique dénotationnelle.
Puisqu'un pomset peut représenter toutes les exécutions possibles d'un processus concurrent, on peut représenter un processus concurrent de notre langage par un unique pomset. Ainsi, on obtient une sémantique déterministe qui permet de modéliser le parallélisme sans avoir recours au choix non déterministe.