Preservation and reflection of bisimilarity via invertible steps

Tools

Turkenburg, Ruben and Kupke, Clemens and Rot, Jurriaan and Schoen, Ezra; Kupferman, Orna and Sobocinski, Pawel, eds. (2023) Preservation and reflection of bisimilarity via invertible steps. In: Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science . Springer, FRA, pp. 328-348. ISBN 9783031308291 (https://doi.org/10.1007/978-3-031-30829-1_16)

[thumbnail of Turkenburg-etal-Springer-2023-Preservation-and-reflection-of-bisimilarity-via-invertible-steps]
Preview
 Text. Filename: Turkenburg_etal_Springer_2023_Preservation_and_reflection_of_bisimilarity_via_invertible_steps.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (924kB)| Preview

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.

CORE (COnnecting REpositories)