A General Account of Coinduction Up-To

Filippo Bonchi (1, 2) , Daniela Petrişan (1, 2) , Damien Pous (1, 2) , Jurriaan Rot (1, 2)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 PLUME - Preuves et Langages

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 modeled as coalgebras. The fact that bisimulations up to context can be safely used in any language specified by GSOS rules can also be seen as an instance of our framework, using the well-known observation by Turi and Plotkin that such languages form bialgebras. In the second part of the paper, we provide a new categorical treatment of weak bisimilarity on labeled transition systems and we prove the soundness of up-to context for weak bisimulations of systems specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. The weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Hence, to reach our goal, we extend the categorical framework developed in the first part to an ordered setting.

Domaines: Logique en informatique [cs.LO]

Filippo Bonchi, Daniela Petrişan, Damien Pous, Jurriaan Rot. A General Account of Coinduction Up-To. Acta Informatica, 2016, ⟨10.1007/s00236-016-0271-4⟩. ⟨hal-01442724⟩