Relators and Notions of Simulation Revisited

TL;DR

The paper develops a unified, coalgebraic approach to (bi)simulation across diverse system types using relators and lax extensions. It establishes core results: (i) coBarr-based bisimulation is sound and complete for functors preserving $1/4$-iso pullbacks, (ii) relationships between relator axioms and closure properties of simulations, and (iii) existence of a greatest normal lax extension for functors that preserve inverse images, enabling a maximally permissive notion of bisimulation. A detailed case study on labelled transition systems introduces twisted bisimulation, a more permissive yet sound and complete notion that remains compositional. The work extends the applicability of behavioural equivalence certification to relational, probabilistic, weighted, neighbourhood-based, and game-based systems and offers new minimization insights for deterministic automata via its greatest-normal-lax-extension framework.

Abstract

Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system types include, for instance, probabilistic, weighted, neighbourhood-based, and game-based systems. Universal coalgebra abstracts system types in this sense as set functors. Notions of (bi)simulation then arise by extending the functor to act on relations in a suitable manner, turning it into what may be termed a relator. We contribute to the study of relators in the broadest possible sense, in particular in relation to their induced notions of (bi)similarity. Specifically, (i) we show that every functor that preserves a very restricted type of pullbacks (termed 1/4-iso pullbacks) admits a sound and complete notion of bisimulation induced by the coBarr relator; (ii) we establish equivalences between properties of relators and closure properties of the induced notion of (bi)simulation, showing in particular that the full set of expected closure properties requires the relator to be a lax extension, and that soundness of (bi)simulations requires preservation of diagonals; and (iii) we show that functors preserving inverse images admit a greatest lax extension. In a concluding case study, we apply (iii) to obtain a novel highly permissive notion of twisted bisimulation on labelled transition systems.

Figures (2)

• Figure 1: Standard bisimulation (left) and alternative additional clauses for twisted bisimulation (right).
• Figure 2: Classes of Relators.

Theorems & Definitions (72)

• Theorem 3.1
• proof
• Corollary 3.2
• Theorem 3.3
• proof
• Theorem 3.4
• proof
• Example 3.5
• Proposition 3.6
• Corollary 3.7