Coinduction up-to in a fibrational setting

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

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

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

Recommendations

• A general account of coinduction up-to
• Enhanced coalgebraic bisimulation
• Beyond Bisimulation: The “up-to” Techniques
• An effective coalgebraic bisimulation proof method
• Coalgebraic bisimulation-up-to

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 (28)

• 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
• Coinductive predicates and final sequences in a fibration
• Bisimulation and coinduction enhancements: a historical perspective
• A fibrational tale of operational logical relations: pure, effectful and differential
• Combining semilattices and semimodules
• Up-to techniques for behavioural metrics via fibrations
• Title not available (Why is that?)
• Behavioural equivalences for timed systems
• Tower induction and up-to techniques for CCS with fixed points
• 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
• 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
• Fibrational bisimulations and quantitative reasoning: extended version
• Products, polynomials and differential equations in the stream calculus
• Convexity via Weak Distributive Laws
• Distribution bisimilarity via the power of convex algebras
• Enhanced coalgebraic bisimulation
• Up-To Techniques for Weighted Systems
• A general account of coinduction up-to
• Companions, codensity and causality

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)