Coinduction-up-to

Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. The use of such techniques dates back to Milner's initial work on bisimilarity. Since then, coinduction up-to proved useful, if not essential, in numerous proofs about concurrent systems; it has been used to obtain decidability results, and more recently to improve standard automata algorithms. We prove the soundness of such techniques in a fibrational setting, building on the seminal work of Hermida and Jacobs. This allows us to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modelled as coalgebras. By tuning the parameters of our framework, we obtain novel techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity. This is joint work with Filippo Bonchi, Daniela Petrisan and Damien Pous. 11: 45 12: 00 Break

Authors

• Jurriaan Rot

Keywords

No keywords are indexed for this paper.