Une sémantique de jeux pour CCS


Tom Hirschowitz, LAMA, LIMD. 8 mars 2012 10:00 limd 2:00:00
Abstract:

On propose une sémantique de jeux pour le langage concurrent CCS (Milner), dont l'ingrédient principal est une catégorie de ``parties'' suffisamment générale pour contenir à la fois une notion de partie en monde clos (quand les joueurs ne peuvent pas interagir avec le monde extérieur) et une notion de vue (ce qu'un joueur retient d'une partie). Les stratégies sont définies sur les vues, puis sont munies (1) d'une opération d'extension à toutes les parties et (2) d'une opération de recollement, qui permet de faire jouer une équipe contre une autre. Ces deux opérations permettent de définir une équivalence de test équitable, analogue à celle donnée indépendamment pour CCS par Cleaveland et al d'une part et Brinksma et al d'autre part, qui compare les stratégies selon leurs réactions à des tests. On donne une traduction de CCS en termes de stratégies et on donne des résultats de comparaison de la sémantique induite avec la bisimilarité faible et avec l'équivalence de test équitable originale.