Coinduction up to in a fibrational setting - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2014

Coinduction up to in a fibrational setting

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.
Fichier principal
Vignette du fichier
cutifs.pdf (347.71 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00936488 , version 1 (26-01-2014)
hal-00936488 , version 2 (15-05-2014)

Identifiers

Cite

Filippo Bonchi, Daniela Petrisan, Damien Pous, Jurriaan Rot. Coinduction up to in a fibrational setting. CSL-LICS, Jul 2014, Vienne, Austria. pp.1-12, ⟨10.1145/2603088.2603149⟩. ⟨hal-00936488v2⟩
259 View
358 Download

Altmetric

Share

Gmail Facebook X LinkedIn More