Coinduction up-to in a fibrational setting

DOI10.1145/2603088.2603149zbMATH Open1395.68195arXiv1401.6675OpenAlexW2077019667MaRDI QIDQ4635603FDOQ4635603

Daniela Petrişan, Jurriaan Rot, Filippo Bonchi, Damien Pous

Publication date: 23 April 2018

Published in: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1401.6675

zbMATH Keywords

similaritybialgebrasfibrationscoinductive predicatesup-to techniquesGSOSbisimulation up-tonominal automata

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Categories of machines, automata (18B20)

Cited In (25)

• Title not available (Why is that?)
• Corecursion up-to via causal transformations
• Predicate and relation liftings for coalgebras with side effects: an application in coalgebraic modal logic
• Bisimulation and coinduction enhancements: a historical perspective
• A fibrational tale of operational logical relations: pure, effectful and differential
• Combining semilattices and semimodules
• Title not available (Why is that?)
• Companions, Codensity and Causality
• Coinduction in Flow: The Later Modality in Fibrations
• Relation lifting, a survey
• Diacritical companions
• Quantitative simulations by matrices
• Up-to techniques for behavioural metrics via fibrations
• Title not available (Why is that?)
• Proving language inclusion and equivalence by coinduction
• Coinduction All the Way Up
• A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata
• Coinductive predicates and final sequences in a fibration
• Products, polynomials and differential equations in the stream calculus
• Convexity via Weak Distributive Laws
• Title not available (Why is that?)
• Up-To Techniques for Behavioural Metrics via Fibrations
• Enhanced coalgebraic bisimulation
• Up-To Techniques for Weighted Systems
• A general account of coinduction up-to

This page was built for publication: Coinduction up-to in a fibrational setting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635603)