Preservation and reflection of bisimilarity via invertible steps

Ruben Turkenburg, Clemens Kupke, Jurriaan Rot, Ezra Schoen

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

1 Citation (Scopus)
18 Downloads (Pure)

Abstract

In the theory of coalgebras, distributive laws give a general perspective on determinisation and other automata constructions. This perspective has recently been extended to include so-called weak distributive laws, covering several constructions on state-based systems that are not captured by regular distributive laws, such as the construction of a belief-state transformer from a probabilistic automaton, and ultrafilter extensions of Kripke frames. In this paper we first observe that weak distributive laws give rise to the more general notion of what we call an invertible step: a pair of natural transformations that allows to move coalgebras along an adjunction. Our main result is that part of the construction induced by an invertible step preserves and reflects bisimilarity. This covers results that have previously been shown by hand for the instances of ultrafilter extensions and belief-state transformers.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
EditorsOrna Kupferman, Pawel Sobocinski
Place of PublicationCham, Switzeraland
PublisherSpringer
Pages328-348
Number of pages21
ISBN (Electronic)9783031308291
ISBN (Print)9783031308284
DOIs
Publication statusPublished - 21 Apr 2023
EventETAPS 2023 - Paris, France
Duration: 22 Apr 202327 Apr 2023
https://etaps.org/2023/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceETAPS 2023
Country/TerritoryFrance
CityParis
Period22/04/2327/04/23
Internet address

Keywords

  • bisimulations
  • coalgebra
  • weak distributive laws

Fingerprint

Dive into the research topics of 'Preservation and reflection of bisimilarity via invertible steps'. Together they form a unique fingerprint.

Cite this