We present a refinement of Pous' companion-based coinductive proof technique and apply it to CCS with general fixed points. We construct companions based on inductive towers and thereby obtain a powerful induction principle. Our induction principle implies a new sufficient condition for soundness of up-to techniques subsuming respectfulness and compatibility. For bisimilarity in CCS, companions yield a notion of relative bisimilarity. We show that relative bisimilarity is a congruence, a basic result implying soundness of bisimulation up-to context. The entire development is constructively formalized in Coq.
Download PDF Show BibTeX
Login to edit