Back to Search
Start Over
Coinduction up to in a fibrational setting
- Source :
- CSL-LICS, Vienne : France (2014)
- Publication Year :
- 2014
-
Abstract
- Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. 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.
Details
- Database :
- arXiv
- Journal :
- CSL-LICS, Vienne : France (2014)
- Publication Type :
- Report
- Accession number :
- edsarx.1401.6675
- Document Type :
- Working Paper
- Full Text :
- https://doi.org/10.1145/2603088.2603149