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

Steven Schäfer; Gert Smolka

Publication details

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

@CONFERENCE{SchaeferSmolka:2017:Tower,
  title = {Tower Induction and Up-To Techniques for CCS with Fixed Points},
  author = {Steven Schäfer and Gert Smolka},
  year = {2017},
  month = {May},
  publisher = {Springer International Publishing},
  booktitle = {Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMiCS 2017, Lyon, France, May 15-18, 2017, Proceedings},
  series = {Lecture Notes in Computer Science},
  volume = {10226},
  pages = {274--289},
}

Legal notice, Privacy policy