Up-to Techniques for Weak Bisimulation

International audienceUp-to techniques have been introduced to enhance the bisim-ulation 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