LSV Seminar

Date

Tuesday, December 04 2012 at 11:00AM

Place

Salle de Conférence (Pavillon des Jardins)

Speaker

Alwen Tiu (Australian National University, Canberra)

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.