Tower Induction and Up-To Techniques for CCS with Fixed Points

Saarland University Computer Science

Steven Schäfer, Gert Smolka

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.


Coq Formalization

Download Sources

Topics in the Paper (toc)