Equations et contextes avec unicité des solutions dans les calculs de processus


Durier Adrien, ENS Lyon. 18 février 2016 10:00 limd 2:00:00
Abstract:

Dans les calculs de processus (ccs, pi-calcul), les bisimulations modulos (up-to) sont des techniques de preuves utilisées pour montrer des équivalences entre processus [1]. Une méthode alternative, mais très similaire, consiste à montrer que deux processus sont solutions d'une même équation [2]. On présentera une telle technique reposant sur la non-divergence d'une solution minimale de l'équation, basée sur [3], qui illustre la correspondance entre bisimulations modulos et unicité des solutions, ainsi que les propriétés attendues d'un contexte dans un cadre abstrait (LTS). [1] Sangiorgi, Davide, and David Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge university press, 2003. [2] Sangiorgi, Davide. Equations, contractions, and unique solutions.'' POPL 2015. [3] Roscoe, A. W.Topology, computer science, and the mathematics of convergence.'' Topology and category theory in computer science. Oxford University Press, Inc., 1991.