The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Observational equivalence, in the context of process calculi, is a notion of behavioral equivalence defined via observable actions of processes. It is commonly defined co-inductively using the transitions of the processes, and, more importantly, it needs to be closed under arbitrary process contexts. Due to the latter requirement, it is difficult to mechanise observational equivalence checking directly, and various methods for approximating observational equivalence have been proposed in the literature. In this talk I will consider an approximation of observational equivalence, for the spi-calculus, based on labelled bisimulation, and present a procedure for checking this notion of bisimulation. This procedure has been implemented in a logical framework called Bedwyr. As the procedure and its implementation are quite complex, to increase confidence in the result of the implemention, the prover (called SPEC) needs to produce an explicit proof object, in terms of a bisimulation set, that can be checked independently outside the prover. Initial experiments suggest that often such a set can be very large, even for simple processes. I will discuss several simplifications to reduce the size of the bisimulation set that are currently implemented in SPEC, exploiting the so-called 'bisimulation-up-to' techniques, originally developed by Milner, Sangiorgi and others for the pi-calculus. I will then discuss some directions for future work, in particular incorporating more general up-to techniques as logical theories in a logical framework.