Coinduction up-to in a fibrational setting

DOI10.1145/2603088.2603149MaRDI QIDQ4635603zbMATH OpenOpenAlexFDO

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)

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)

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.

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

Cited in

(28)

• Companions, codensity and causality
• scientific article; zbMATH DE number 7449991 (Why is no real title available?)
• Coinductive predicates and final sequences in a fibration
• 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
• Combining semilattices and semimodules
• A fibrational tale of operational logical relations: pure, effectful and differential
• Up-to techniques for behavioural metrics via fibrations
• Behavioural equivalences for timed systems
• scientific article; zbMATH DE number 7204940 (Why is no real title available?)
• Tower induction and up-to techniques for CCS with fixed points
• Relation lifting, a survey
• Coinduction in Flow: The Later Modality in Fibrations
• Diacritical companions
• Quantitative simulations by matrices
• Up-to techniques for behavioural metrics via fibrations
• Proving language inclusion and equivalence by coinduction
• A generalized partition refinement algorithm, instantiated to language equivalence checking for weighted automata
• Coinduction All the Way Up
• 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
• Up-To Techniques for Weighted Systems
• Enhanced coalgebraic bisimulation
• 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)