A general account of coinduction up-to
type: Item
instance of: scholarly article
title: A general account of coinduction up-to
zbMATH Open document ID: 1371.68186
author: Filippo Bonchi
author: Daniela Petrişan
author: Damien Pous
author: Jurriaan Rot
published in: Acta Informatica
publication date: 2017-04-20T00:00:00Z
review text: Up-to techniques were introduced in [\textit{R. Milner}, Communication and concurrency. New York etc.: Prentice Hall (1989; Zbl 0683.68008)]. The authors of the paper under review prove the soundness of such techniques in a fibrational setting, building on the work [\textit{C. Hermida} and \textit{B. Jacobs}, Inf. Comput. 145, No. 2, 107--152 (1998; Zbl 0941.18006)]. This allows them to systematically obtain up-to techniques not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. For instance, the fact that bisimulations up to context can be safely used in any language specified by GSOS rules can also be proved in the proposed framework by exploiting the well-known observation by Turi and Plotkin that such languages form bialgebras [\textit{D. Turi} and \textit{G. D. Plotkin}, ``Towards a mathematical operational semantics'', in: Proceedings of the twelfth annual IEEE symposium on logic in computer science, LICS '97. Los Alamitos: IEEE Computer Society Press. 280--291 (1997)]. In the second part of the paper, the soundness of up-to contextual closure for weak bisimulations of systems is specified by cool rule formats, as defined by Bloom to ensure congruence of weak bisimilarity. However, the weak transition systems obtained from such cool rules give rise to lax bialgebras, rather than to bialgebras. Thus, the categorical framework developed in the first part is extended to an ordered setting. This paper is an extended version of [the authors, ``Coinduction up-to in a fibrational setting'', in: Proceedings of the joint meeting of the 23rd EACSL annual conference on computer science logic (CSL) and the 29th annual ACM/IEEE symposium on logic in computer science, CSL-LICS'14. New York, NY: Association for Computing Machinery (ACM). Article No. 20, 9 p. (2014; \url{doi:10.1145/2603088.2603149}); LIPICS -- Leibniz Int. Proc. Inform. 42, 240--253 (2015; Zbl 1371.68187)]. Section 2 contains motivating examples. Coinduction and up-t…
reviewed by: Ahmet A. Khusainov
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 6706473
zbMATH Keywords: up-to techniques
zbMATH Keywords: weak bisimulation
zbMATH Keywords: lax bialgebras
zbMATH Keywords: coinductive predicates
zbMATH Keywords: coalgebras
MaRDI profile type: Publication
full work available at URL: s00236-016-0271-4
OpenAlex ID: W2468444917
cites work: Structural operational semantics.
cites work: Finitary Functors: From Set to Preord and Poset
cites work: Positive Fragments of Coalgebraic Logics
cites work: Generalised coinduction
cites work: Structural operational semantics for weak bisimulations
cites work: Bisimulation can't be traced
cites work: Turing Machines with Atoms
cites work: A coalgebraic perspective on linear weighted automata
cites work: Coinduction up-to in a fibrational setting
cites work: Lax Bialgebras and Up-To Techniques for Weak Bisimulations
cites work: Checking NFA equivalence with bisimulations up to congruence
cites work: Weak bisimulation for coalgebras over order enriched monads
cites work: Behavioural equivalences for coalgebras with unobservable moves
cites work: Derivatives of Regular Expressions
cites work: Graphes canoniques de graphes algébriques
cites work: Branching time and abstraction in bisimulation semantics
cites work: A congruence rule format for name-passing process calculi
cites work: Coalgebraic Weak Bisimulation from Recursive Equations over Monads
cites work: Coinductive predicates and final sequences in a fibration
cites work: Structural induction and coinduction in a fibrational setting
cites work: Simulations in coalgebra
cites work: Categorical logic and type theory
cites work: An effective coalgebraic bisimulation proof method
cites work: Bialgebras for structural operational semantics: an introduction
cites work: Q4256307
cites work: Q4499306
cites work: Q3992568
cites work: Q4222939
cites work: Q4035257
cites work: Nominal sets. Names and symmetry in computer science
cites work: Complete Lattices and Up-To Techniques
cites work: Enhancements of the bisimulation proof method
cites work: Enhanced coalgebraic bisimulation
cites work: Universal coalgebra: A theory of systems
cites work: On the bisimulation proof method
cites work: Introduction to Bisimulation and Coinduction
cites work: Generalizing the powerset construction, coalgebraically
cites work: Sequent calculi for process verification: Hennessy-Milner logic for an arbitrary GSOS
cites work: Probabilistic systems coalgebraically: a survey
cites work: Q4621137
cites work: Relating coalgebraic notions of bisimulation
cites work: Q4092156
cites work: Fixpoint semantics and simulation
cites work: On cool congruence formats for weak bisimulations
DOI: 10.1007/S00236-016-0271-4
description: scientific article; zbMATH DE number 6706473