From observational to symbolic to static equivalence

Add to your list(s) Download to your calendar using vCal

• Sergiu Bursuc
• Tuesday 08 June 2010, 13:00-14:00
• CS 124.

If you have a question about this talk, please contact Dan Ghica.

Observational equivalence is a fundamental notion in reasoning about the semantics of processes: it holds when two processes behave in the same way in a given environment, independent of details in their implementation. On the other hand, static equivalence is about data: it holds when two sets of data are indistinguishable for an observer, no matter the experiments he takes. In formal methods, data is represented by first order terms, processes are described by an algebra, interaction with processes is defined by an operational semantics and interaction with data by logical proofs.

In this setting, an interesting practical (and theoretical) problem is finding decision procedures for observational and static equivalence. This problem is parametrized by a logical theory that captures the properties of data (e.g. associativity, commutativity, xor, encryptions and decryptions) and relates to, but generalizes in many ways, the problem of proof search in the given theory.

In two talks at lab lunch I will show that one can, remarkably, unravel the dynamics of processes and reduce observational equivalence to static equivalence. Roughly, this amounts to reducing an infinite number of traces (the possible observations of the environment) to a finite number of sets that capture staticly all the relevant information. The intermediate step of this reduction is symbolic equivalence, where we group similar traces into formal objects called constraint systems. The transition from observational to symbolic equivalence is the subject of my first talk, and is based on works of Joost Engelfriet, Stephanie Delaune and Veronique Cortier.

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• CS 124
• Lab Lunch

Note that ex-directory lists are not shown.