Publication details

Saarland University Computer Science

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

Steven Schäfer, Gert Smolka

Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings, Vol. 10226 of Lecture Notes in Computer Science, pp. 274--289, Springer International Publishing, May 2017

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.

Formalization

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy