Travaux anciens

Dans un premier temps [15], je me suis surtout intéressé aux aspects sémantiques du parallélisme en définissant une sémantique qui permette de prendre en compte les problèmes d'équité pour le langage CSP de Hoare. Le problème essentiel concernait les questions d'équité (fairness) qui amènent à prendre en compte les comportements infinis des processus. L'ensemble des comportements étant considéré comme un langage infinitaire, on peut utiliser des outils et résultats classiques comme, par exemple, les automates, pour la vérification de propriétés.

De façon indépendante, je me suis aussi intéressé à la caractérisation des problèmes qui peuvent être traités de façon optimale de façon parallèle. Certains des résultats obtenus sont résumés dans [16].

Pour les systèmes distribués, il paraît plus naturel de considérer un calcul distribué comme un ensemble d'évènements avec une relation d'ordre partiel: la relation de causalité de Lamport. Dans [17], nous nous sommes intéressés à des propriétés des calculs vérifiées par certains états globaux du système (transformateurs de prédicats possibly et definively).