In 2005, we proposed a theory for up-to techniques for bisimilarity, in this paper, that appeared in the proceedings of ICALP'05. An extended version appeared in TCS since; slides for ICALP05 are available here (printable version).
Abstract (05): Up-to techniques have been introduced to
enhance the bisimulation proof method for establishing bisimilarity
results. While up-to techniques for strong bisimilarity are well
understood, in the weak case they come as a collection of unrelated
results, and lack a unified presentation.
We propose a uniform and modular theory of up-to techniques for
weak bisimulation that captures existing proof technology and
introduces new techniques. Some proofs rely on non trivial -- and new
-- commutation results based on termination guarantees.
The flexibility and usefulness of our framework is illustrated on
two examples, one of them coming from a recent study of a distributed
abstract machine.
All the results of the first paper have been formalised and checked using the COQ Proof Assistant. Here are the COQ sources (under GPL). Here is the coqdoc generated documentation (the numbering of results corresponds to the published - short - paper). The developments are structured as follows:
In 2006, we extended this work in this CONCUR paper. Here are a long version, with full proofs, the slides, and printable slides.
Abstract (06): We study the use of the elaboration
preorder (due to Arun-Kumar and Natarajan) in the framework of up-to
techniques for weak bisimulation. We show that elaboration yields a
correct technique that encompasses the commonly used up to expansion
technique. We also define a theory of up-to techniques for elaboration
that in particular validates an elaboration up to elaboration
technique, while it is known that weak bisimulation up to weak
bisimilarity is unsound. In this sense, the resulting setting
improves over previous works in terms of modularity.
Our results are obtained using nontrivial proofs that exploit
termination arguments. In particular, we need the termination of
internal computations for the up-to techniques to be correct. We show
how this condition can be relaxed to some extent in order to handle
processes exhibiting infinite internal behaviour.
In 2007, we defined a more general theory of up-to techniques for coinduction (presented at APLAS; here are the slides and printable slides).
Abstract (07): We propose a theory of up-to techniques
for proofs by coinduction, in the setting of complete lattices. This
theory improves over existing results by providing a way to compose
arbitrarily complex techniques with standard techniques, expressed
using a very simple and modular semi-commutation property.
Complete lattices are enriched with monoid operations, so that we
can recover standard results about labelled transitions systems and
their associated behavioural equivalences at an abstract,
``point-free'' level.
Our theory gives for free a powerful method for validating up-to
techniques. We use it to revisit up to contexts techniques, which
are known to be difficult in the weak case: we show that it is
sufficient to check basic conditions about each operator of the
language, and then rely on an iteration technique to deduce general
results for all contexts.