1 Introduction
Notions of simulation and bisimulation are pervasive in the specification and verification of reactive systems (e.g. [31]). For instance, they appear in state space reduction (e.g. [6]), they are used to specify concrete systems in terms of abstract systems (e.g. in connection with the analysis of ePassport protocols [22]), and, classically, they relate tightly to indistinguishability in modal logic [19]. Originally introduced for (labelled) transition systems, notions of (bi)simulation have been extended to a wide range of system types, e.g. probabilistic systems [10, 27], weighted systems [9], or monotone neighbourhood frames [17, 34]. They have received a uniform treatment in the framework of universal coalgebra [37]. However, so far, notions of (bi)simulation have typically been confined to settings where the two systems being compared are of the same type in a strict sense, e.g. labelled transition systems (LTS) over the same alphabet. In the present paper, we introduce a principled approach to comparing behaviour across different system types by means of heterogeneous (bi)simulations.
To this end, we encapsulate system types as set functors in the paradigm of universal coalgebra, and introduce (relational) connectors between system types. The latter generalize lax extensions, which induce notions of (bi)simulation on a single system type [29, 30]. A connector between functors F and G induces a notion of (bi)simulation between F-coalgebras and G-coalgebras, i.e. between the systems of the types represented by F and G, respectively, for instance between nondeterministic and probabilistic systems. We give a range of constructions of connectors, such as converse, composition, and pulling back along natural transformations. Notably, we show that the composition of relational connectors admits identities. Identity relational connectors satisfy a minimality condition, and form smallest lax extensions of functors; for weak-pullback-preserving functors, they coincide with the Barr extension [5], which instantiates, e.g., to the well-known Egli-Milner relation lifting for the powerset functor. We use these constructions to cover a number of application scenarios, e.g. transferring bisimilarity among LTS over different alphabets; sharing of infinite traces among LTS; nondeterministic abstractions of probabilistic LTS; and input-output conformances (ioco) [8].
Anzeige
We go on to give a construction of relational connectors based on relating modalities, modelled as predicate liftings in the style of coalgebraic logic [33, 38]. In reference to constructions of behavioural metrics (on a single system type) from modalities [3, 47], we call such relational connectors Kantorovich. Many of our running examples turn out to be Kantorovich. We then prove a Hennessy-Milner-type result for Kantorovich connectors, showing that on finitely branching systems, the induced similarity coincides with theory inclusion in a generic dual-purpose modal logic that can be interpreted over both of the involved system types. The generic theorem instantiates to logical characterizations of bisimulation between LTS with different alphabets, trace sharing between LTS, nondeterministic abstraction of probabilistic LTS, and ioco compatibility.
Proofs are often omitted or only sketched; details can be found in the full version [32].
Related work Relational connectors generalize lax extensions [29, 30, 39, 40], which belong to an extended strand of work on extending set functors to act on relations (e.g. [2, 21, 28, 42]). The Kantorovich construction similarly generalizes constructions of functor liftings and lax extensions in both two-valued and quantitative settings [3, 13, 16, 29, 30, 47]. Our heterogeneous Hennessy-Milner theorem generalizes (the monotone case of) coalgebraic Hennessy-Milner theorems for behavioural equivalence [33, 38] and behavioural preorders [23, 46]. A different generalization of notions of bisimulation occurs via functor liftings along fibrations [18, 20], which have also been connected to modal logics [24, 25]. The Kantorovich construction is generalized there by the so-called codensity lifting [41]. Heterogeneous notions of bisimulation have not been considered there.
2 Preliminaries: Coalgebras and Lax Extensions
We assume basic familiarity with category theory (e.g. [1]). We proceed to recall requisite background on relations, coalgebras, and lax extensions.
Anzeige
Relations A relation from a set X to a set Y is a subset \(r\subseteq X\times Y\), denoted \(r:X\, |\!\!\!\!\rightarrow Y\); we write \(x\mathrel {r}y\) for \((x,y)\in r\). Given \(r:X\, |\!\!\!\!\rightarrow Y\) and \(s:Y\, |\!\!\!\!\rightarrow Z\), we write \(s\cdot r\) for the applicative-order relational composite of r and s, i.e.The join of a family of relations is just its union. Relational composition is join continuous in both arguments, i.e. we have \((\bigvee _{i\in I}s_i)\cdot r=\bigvee _{i\in I}(s_i\cdot r)\) and \(s\cdot (\bigvee _{i\in I}r_i)=\bigvee _{i\in I}(s\cdot r_i)\). We define the relational converse \(r ^ \circ :Y\, |\!\!\!\!\rightarrow X\) by \( r ^ \circ =\{(y,x)\mid (x,y)\in r\}. \) We identify a function \(f:X\rightarrow Y\) with its graph, i.e. the relation \(\{(x,f(x))\mid x\in X\}\). For clarity, we sometimes write \( \varDelta _X=\{(x,x)\mid x\in X\} \) for the diagonal relation on X, i.e. the graph of the identity function on X, which is neutral for relational composition. Functions \(f:X\rightarrow Y\) are characterized by the inequalitiesGiven a subset \(A\subseteq X\) and a relation \(r:X\, |\!\!\!\!\rightarrow Y\), we write \(r[A]=\{y\in Y\mid \exists x\in A.\,x\mathrel {r}y\}\) for the relational image of A under r. We say that r is right total if \(r[X]=Y\), and left total if \(r ^ \circ [Y]=X\).
$$\begin{aligned} s\cdot r=\{(x,z)\mid \exists y\in Y.\,x\mathrel {r}y\mathrel {s}z\}. \end{aligned}$$
$$\begin{aligned} \varDelta _X\subseteq f ^ \circ \cdot f\quad {{(totality)}} \qquad f\cdot f ^ \circ \subseteq \varDelta _Y \quad {{(univalence)}.} \end{aligned}$$
Universal coalgebra State-based systems of a wide range of transition types can be usefully abstracted as coalgebras for a given functor encapsulating the system type [37]. We work more specifically over the category of sets, and thus model a system type as a functor \(F:\textsf{Set}\rightarrow \textsf{Set}\). Then, an F-coalgebra is a pair \((C,\gamma )\) consisting of a set C of states and a transition map \(\gamma :C\rightarrow FC\). Following tradition in algebra, we often just write C for the coalgebra \((C,\gamma )\). We think of C as a set of states, and of \(\gamma \) as assigning to each state \(c\in C\) a collection \(\gamma (c)\) of successor states, structured according to F. For instance, if \(F=\mathcal {P}\) is the usual (covariant) powerset functor, then \(\gamma \) assigns to each state a set of successors, so a \(\mathcal {P}\)-coalgebra is just a standard relational transition system. More generally, given a set \(\mathcal {A}\) of labels, F-coalgebras for the functor \(F=\mathcal {P}(\mathcal {A}\times (-))\) are \(\mathcal {A}\)-labelled transition systems (\(\mathcal {A}\)-LTS). On the other hand, we write \(\mathcal {D}\) for the (discrete) distribution functor, which assigns to a set X the set of discrete probability distributions on X (which may be represented as functions \(\alpha :X\rightarrow [0,1]\) such that \(\sum _{x\in X}\alpha (x)=1\), extended to subsets \(A\subseteq X\) by \(\alpha (A)=\sum _{x\in A}\alpha (x)\)) and acts on maps by taking direct images. Then, \(\mathcal {D}\)-coalgebras are probabilistic transition systems, or Markov chains, while \(\mathcal {D}(\mathcal {A}\times (-))\)-coalgebras are probabilistic \(\mathcal {A}\)-labelled transition systems (probabilistic \(\mathcal {A}\)-LTS). We assume w.l.o.g. that functors preserve injective maps [5], and then in fact that subset inclusions are preserved.
A morphism \(f:C\rightarrow D\) of F-coalgebras \((C,\gamma )\), \((D,\delta )\) is a map \(f:C\rightarrow D\) such that \(Ff\cdot \gamma =\delta \cdot f\). States \(c\in C\), \(d\in D\) in F-coalgebras C, D are behaviourally equivalent if there exist an F-coalgebra \((E,\epsilon )\) and morphisms \(f:C\rightarrow E\), \(g:D\rightarrow E\) such that \(f(x)=g(y)\). For instance, morphisms of \(\mathcal {P}(\mathcal {A}\times (-))\)-coalgebras are bounded morphisms of \(\mathcal {A}\)-LTS in the usual sense (i.e. functional bisimulations), and behavioural equivalence instantiates to the usual notion of (strong) bisimilarity on LTS.
Lax extensions As indicated in the introduction, relational connectors are largely intended as a generalization of lax extensions, which extend a single functor to act also on relations, to settings where relations need to connect elements of different functors. A lax extension L (references are in Section 1) of a set functor F assigns to each relation \(r:X\, |\!\!\!\!\rightarrow Y\) a relation \(Lr:FX\, |\!\!\!\!\rightarrow FY\) such thatfor all sets X, Y, Z, and \(r,r_1,r_2:X\, |\!\!\!\!\rightarrow Y\), \(s:Y\, |\!\!\!\!\rightarrow Z\), \(f:X\rightarrow Y\). These conditions imply naturality [30, 40]:for \(r:X\, |\!\!\!\!\rightarrow Y\) and maps \(f:X'\rightarrow X\), \(g:Y'\rightarrow Y\). We say that L preserves diagonals if \( L\varDelta _X \subseteq \varDelta _{FX}\text { for all}~{ X}, \) equivalently, \(L f \subseteq F f\) for all maps f. Moreover, L preserves converse if \(L(r ^ \circ )=(Lr) ^ \circ \) for all r. (Indeed, this property is often included in the definition of lax extension [30].)
$$\begin{aligned} \text {(L1)} &\quad r_1 \subseteq r_2 \rightarrow Lr_1 \subseteq Lr_2 &\,&{{(monotonicity)}} \\ \text {(L2)} &\quad Ls\cdot Lr \subseteq L(s\cdot r) &\,&{{(lax\ functoriality)}}\\ \text {(L3)} &\quad Ff\subseteq Lf \text { and } (Ff) ^ \circ \subseteq L(f ^ \circ ) \end{aligned}$$
$$\begin{aligned} L(g ^ \circ \cdot r\cdot f)=(Fg) ^ \circ \cdot Lr\cdot Ff \end{aligned}$$
Lax extensions induce notions of (bi)simulation, that is, of relations that witness behavioural equivalence in the sense recalled above. Given a lax extension L of a functor F, a relation \(r:C\, |\!\!\!\!\rightarrow D\) between F-coalgebras \((C,\gamma )\), \((D,\delta )\) is an L-simulation if \(\delta \cdot r\le Lr\cdot \gamma \); that is, whenever \(c\mathrel {r}d\), then \(\gamma (c)\mathrel {Lr}\delta (d)\). Two states \(c\in C\), \(d\in D\) are L-similar if there exists an L-simulation \(r:C\, |\!\!\!\!\rightarrow D\) such that \(c\mathrel {r}d\). If L preserves converse, then the converse \(r ^ \circ \) of an L-simulation r is also an L-simulation and, hence, L-similarity is symmetric; one thus speaks more appropriately of L-bisimulations and L-bisimilarity. Notably, if L preserves converse and diagonals, then L-bisimilarity coincides with behavioural equivalence [29, 30]. Every lax extension can be induced from a choice of modalities [29, 30]; we return to this point in Section 5. We recall only the most basic example:
Example 2.1
Let \(\mathcal {A}\) be a set of labels, and let \(F=\mathcal {P}(\mathcal {A}\times (-))\) be the functor modelling \(\mathcal {A}\)-LTS as recalled above. We have a converse- and diagonal-preserving lax extension L of F given by \(S\mathrel {Lr}T\) iff (i) for all \((l,x)\in S\), there is \((l,y)\in T\) such that \(x\mathrel {r}y\) (‘forth’), and (ii) for all \((l,y)\in T\), there is \((l,x)\in S\) such that \(x\mathrel {r}y\) (‘back’). Indeed, L is even a strict extension, i.e. condition (L2) holds in the stronger form \(Ls\cdot Lr=L(s\cdot r)\) for composable s, r (such strict extensions exist, and then are unique, iff the underlying functor preserves weak pullbacks [4, 44]). L-bisimulations in the sense recalled above are precisely (strong) bisimulations of LTS in the standard sense.
Remark 2.2
(Barr extension). The above-mentioned strict extension L of a weak-pullback-preserving functor F, often called the Barr extension, is described as follows [4]: A relation \(r:X\, |\!\!\!\!\rightarrow Y\) itself forms a set (a subset of \(X\times Y\)), and as such comes with two projection maps \(\pi _1:r\rightarrow X\), \(\pi _2:r\rightarrow Y\). Then, \(Lr=F\pi _2\cdot (F\pi _1) ^ \circ \). A slightly simpler example than Example 2.1 is the Barr extension L of the powerset functor \(\mathcal {P}\), which coincides with the well-known Egli-Milner extension: For \(r:X\, |\!\!\!\!\rightarrow Y\) and \(S\in \mathcal {P}(X)\), \(T\in \mathcal {P}(Y)\), we have \(S\mathrel {Lr}T\) iff for every \(x\in S\) there is \(y\in T\) such that \(x\mathrel {r}y\) and symmetrically.
3 Relational Connectors
We proceed to introduce relational connectors and associated constructions.
3.1 Axiomatics
The main idea is that while a lax extension of a functor F (Section 2) lifts relations between sets X and Y to relations between FX and FY, a relational connector between functors F and G lifts relations between sets X and Y to relations between FX and GY. The axiomatics of relational connectors is inspired by that of lax extensions, but forcibly deviates in some respects:
Definition 3.1
(Relational connector). Let F, G be set functors. A relational connector (or occasionally just a connector) \(L:F\rightarrow G\) assigns to each relation \(r:X\, |\!\!\!\!\rightarrow Y\) a relationsuch that the following conditions hold:
$$\begin{aligned} Lr:FX\, |\!\!\!\!\rightarrow GY \end{aligned}$$
1.
Whenever \(r_1\subseteq r_2\) for \(r_1,r_2:X\, |\!\!\!\!\rightarrow Y\), then \(Lr_1\subseteq Lr_2\) (monotonicity).
2.
Whenever \(f:X'\rightarrow X\), \(g:Y'\rightarrow Y\), and \(r:X\, |\!\!\!\!\rightarrow Y\), then
$$\begin{aligned} L(g ^ \circ \cdot r\cdot f)=(Gg) ^ \circ \cdot Lr\cdot Ff\qquad {({naturality}).} \end{aligned}$$
We define an ordering on connectors \(F\rightarrow G\) by \(L\le K\) iff \(Lr\subseteq Kr\) for all r.
In pointful notation, naturality says that for data as above and \(a\in FX'\), \(b\in GY'\), we have
$$\begin{aligned} Ff(a)\mathrel {Lr}Gg(b)\quad \text {iff}\quad a\mathrel {L(g ^ \circ \cdot r\cdot f)}b. \end{aligned}$$
(3.1)
Example 3.2
Let \(F=\mathcal {P}(\mathcal {A}\times (-))\), \(G=\mathcal {P}(\mathcal {B}\times (-))\) be the functors determining \(\mathcal {A}\)-LTS and \(\mathcal {B}\)-LTS as their coalgebras, respectively (Section 2). For \(R\subseteq \mathcal {A}\times \mathcal {B}\), we define a relational connector \(L_R:F\rightarrow G\) byfor \(r:X\, |\!\!\!\!\rightarrow Y\). We will later use instances of this type of relational connector to transfer bisimilarity between \(\mathcal {A}\)-LTS and \(\mathcal {B}\)-LTS.
$$\begin{aligned} S\mathrel {L_Rr}T \iff \forall (l,m)\in R. & \;\forall (l,x)\in S.\,\exists (m,y)\in T.\,x\mathrel {r}y\;\wedge \\ & \;\forall (m,y)\in T.\,\exists (l,x)\in S.\,x\mathrel {r}y \end{aligned}$$
Of course, every lax extension of F is a relational connector \(F\rightarrow F\). In the axiomatics of relational connectors, notable omissions in comparison to lax extensions include (L2) and (L3), both of which in general just fail to type for relational connectors. We will later discuss these conditions and further ones as properties that a relational connector may or may not have, if applicable. Note that we do retain an important consequence of these properties, viz., naturality.
3.2 Constructions
Our perspective on relational connectors is partly driven by constructions enabled by the axiomatics; maybe the most central ones among these are composition and identities, introduced next.
Definition 3.3
(Composition of relational connectors). Given relational connectors \(K:F\rightarrow G\), \(L:G\rightarrow H\), we define the composite \(L\cdot K:F\rightarrow H\) bywhere the join is over all \(t:X\, |\!\!\!\!\rightarrow Y\), \(s:Y\, |\!\!\!\!\rightarrow Z\) such that \(s\cdot t=r\), with Y ranging over all sets (see however Theorem 3.8 and Lemma 3.5).
$$\begin{aligned} (L\cdot K)r=\bigvee _{r=s\cdot t}Ls\cdot Kt\quad \text {for }r:X\, |\!\!\!\!\rightarrow Z, \end{aligned}$$
(3.2)
Lemma 3.4
Given relational connectors \(K:F\rightarrow G\), \(L:G\rightarrow H\), the composite \(L\cdot K:F\rightarrow H\) is a relational connector.
Proof (sketch)
Monotonicity: Let \(r\subseteq r':X\, |\!\!\!\!\rightarrow Z\). If \(a\;(L\cdot K)r\;c\) is witnessed by a factorization \(r=s\cdot t\) where \(t:X\, |\!\!\!\!\rightarrow Y\), \(s:Y\, |\!\!\!\!\rightarrow Z\), then \(a\;(L\cdot K)r'\;c\) is witnessed by the factorization \(r'=s'\cdot t'\) where \(t':X\, |\!\!\!\!\rightarrow Y'\), \(s':Y'\, |\!\!\!\!\rightarrow Z\) with \(Y'=Y\cup (r'\setminus r)\) (w.l.o.g. a disjoint union) andRemarkably, the further proof uses naturality (w.r.t. \(Y\hookrightarrow Y'\)) but not monotonicity of K and L.
$$\begin{aligned} t'=t\cup \{(x,(x,z))\mid (x,z)\in r'\setminus r\}\qquad s'=s\cup \{((x,z),z)\mid (x,z)\in r'\setminus r\}. \end{aligned}$$
Naturality: \((L\cdot K)(g ^ \circ \cdot r\cdot f)=(Hg) ^ \circ \cdot (L\cdot K)r\cdot Ff\) is shown using naturality and monotonicity of K and L, monotonicity of \(L\cdot K\), and totality and univalence of f and g. \(\square \)
As an immediate consequence of monotonicity of composite relational connectors, we have the following alternative description of composition:
Lemma 3.5
Given relational connectors \(K:F\rightarrow G\), \(L:G\rightarrow H\), we havewhere the join is over all \(t:X\, |\!\!\!\!\rightarrow Y\), \(s:Y\, |\!\!\!\!\rightarrow Z\) such that \(r\supseteq s\cdot t\), with Y ranging over all sets.
$$\begin{aligned}\textstyle (L\cdot K)r=\bigvee _{r\supseteq s\cdot t}Ls\cdot Kt\quad \text {for }r:X\, |\!\!\!\!\rightarrow Z \end{aligned}$$
In order to compute composites of relational connectors, the following observation is sometimes useful.
Definition 3.6
The couniversal factorization \(r=s\cdot t\) of a relation \(r:X\, |\!\!\!\!\rightarrow Z\) is given by
$$\begin{aligned} Y & =\{(A,B)\in \mathcal {P}(X)\times \mathcal {P}(Z)\mid A\times B\subseteq r\}\\ t & =\{(x,(A,B))\mid x\in A\}:X\, |\!\!\!\!\rightarrow Y\\ s & =\{((A,B),z)\mid z\in B\}:Y\, |\!\!\!\!\rightarrow Z. \end{aligned}$$
Lemma 3.7
Let \(s:Y\, |\!\!\!\!\rightarrow Z\), \(t:X\, |\!\!\!\!\rightarrow Y\) be the couniversal factorization of \(r:X\, |\!\!\!\!\rightarrow Z\). Then indeed \(r=s\cdot t\), and for every factorization \(r=s'\cdot t'\) of r into \(s':Y'\, |\!\!\!\!\rightarrow Z\), \(t':X\, |\!\!\!\!\rightarrow Y'\), there is a map \(f:Y'\rightarrow Y\) such that \(s' = s \cdot f\) and \(t' = f ^ \circ \cdot t\).
Theorem 3.8
Let \(K:F\rightarrow G\), \(L:G\rightarrow H\) be relational connectors, and let \(r=s\cdot t\) be the couniversal factorization of \(r:X\, |\!\!\!\!\rightarrow Z\). Then
$$\begin{aligned} (L\cdot K)r=Ls\cdot Kt. \end{aligned}$$
We proceed to establish that the composition operation defined above equips relational connectors with the structure of a quasicategory (i.e. overlarge category). We first check associativity:
Lemma 3.9
Let \(K:F\rightarrow G\), \(L:G\rightarrow H\), and \(M:H\rightarrow V\) be relational connectors. Then \((M\cdot K)\cdot L=M\cdot (K\cdot L)\).
The straightforward proof uses join continuity of relational composition. We next construct identities:
Definition 3.10
(Identity relational connectors). The identity relational connector \(\textsf{Id}^\textsf{c}_{F}:F\rightarrow F\) on a set functor F is defined as follows. For \(r:X\, |\!\!\!\!\rightarrow Y\), \(b\in FX\), and \(c\in FY\), we put \(b\mathrel {\textsf{Id}^\textsf{c}_{F}r} c\) iff for all set functors G, all relational connectors \(L:G\rightarrow F\), all \(s:Z\, |\!\!\!\!\rightarrow X\), and all \(a\in GZ\),
$$\begin{aligned} a\mathrel {Ls}b\quad \text {implies}\quad a\mathrel {L(r \cdot s)}c. \end{aligned}$$
(This definition is highly impredicative, but we will later give a characterization of \(\textsf{Id}^\textsf{c}_{F}\) that eliminates quantification over relational connectors.) We will show that \(\textsf{Id}^\textsf{c}_{F}\) is neutral w.r.t. composition of relational connectors. We first note that, as an immediate consequence of the definition,
$$\begin{aligned} \varDelta _{FX}\subseteq \textsf{Id}^\textsf{c}_{F}\varDelta _X\qquad \text {for all}~X. \end{aligned}$$
(3.3)
Lemma 3.11
For each functor F, \(\textsf{Id}^\textsf{c}_{F}\) is a relational connector.
The proof of naturality relies in particular on monotonicity of relational connectors in combination with totality and univalence of maps. We show next that identity connectors do actually act as identities under composition:
Lemma 3.12
For each \(L:G\rightarrow F\), we have \(L=\textsf{Id}^\textsf{c}_{F}\cdot L=L\cdot \textsf{Id}^\textsf{c}_{G}\).
Proof (sketch)
One shows, using (3.3) inter alia, that \(\textsf{Id}^\textsf{c}_{F}\) is a left identity (\(L=\textsf{Id}^\textsf{c}_{F}\cdot L\)). By a symmetric argument, composition of relational connectors also has right identities, and then the left and right identities are necessarily equal. \(\square \)
Relational connectors admit a natural notion of converse:
Definition 3.13
(Converse, meet and product of relational connectors). The converse \(L ^ \circ :G\rightarrow F\) of a relational connector \(L:F\rightarrow G\) is given byfor \(r:X\, |\!\!\!\!\rightarrow Y\). The meet \(L\cap K\) of relational connectors \(L,K:F\rightarrow G\) is their componentwise intersection (\((L\cap K)r=Lr\cap Kr\)). For relational connectors \(L_1 :F_1 \rightarrow G_1\) and \(L_2 :F_2 \rightarrow G_2\), their product \(L_1 \times L_2 :F_1 \times F_2 \rightarrow G_1 \times G_2\) is given by
$$\begin{aligned} L ^ \circ r=(Lr ^ \circ ) ^ \circ :GX\, |\!\!\!\!\rightarrow FY \end{aligned}$$
$$\begin{aligned} (a,b) \mathrel {(L_1 \times L_2) r} (c,d) \iff a \mathrel {L_1 r} c \text { and } b \mathrel {L_2 r} d. \end{aligned}$$
Lemma 3.14
The converse, meet and product of relational connectors are again relational connectors.
We record some expected properties of converse:
Lemma 3.15
Converse is involutive (\((L ^ \circ ) ^ \circ =L\)) and monotone. Moreover, for relational connectors \(K:F\rightarrow G\) and \(L:G\rightarrow H\), we have
$$\begin{aligned} (L\cdot K) ^ \circ =K ^ \circ \cdot L ^ \circ . \end{aligned}$$
Remark 3.16
In view of the above properties, one may ask whether relational connectors form an overlarge allegory [12]. We leave this question open for the moment; specifically, it is not clear that relational connectors satisfy the modular law \((L\cdot K)\cap M \le L\cdot (K\cap (L ^ \circ \cdot M))\).
Example 3.17
(Constructions of relational connectors). We can decompose the connector \(L_R:\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {B}\times (-))\) from Example 3.2 as follows. Define a further relational connector \(K_R:\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {B}\times (-))\) similarly as \(L_R\) but omit one of the directions, putting \(S\mathrel {K_Rr}T\) (for \(S\in \mathcal {P}(\mathcal {A}\times X)\), \(T\in \mathcal {P}(\mathcal {B}\times Y)\), and \(r:X\, |\!\!\!\!\rightarrow Y\)) iff for all \((l,m)\in R\) and \((l,x)\in S\), there is \((m,y)\in T\) such that \(x\mathrel {r}y\). While \(L_R\) has the feel of inducing a notion of heterogeneous bisimilarity (this will be made formal in Section 4), \(K_R\) has a flavour of similarity, including as it does only a ‘forth’-type condition. Clearly, we haveGiven a further set \(\mathcal {C}\) of labels and a relation \(Q\subseteq \mathcal {B}\times \mathcal {C}\), we haveIt is a fairly typical phenomenon in describing composites of relational connectors that upper bounds such as the above are often straightforward, while the converse inequalities are more elusive or fail to hold. When showing \( K_{Q\cdot R}\,r\subseteq (K_Q\cdot K_R)\,r\) for \(r:X\, |\!\!\!\!\rightarrow Z\), one gets away with using the trivial factorization \(r=s\cdot t\) given by \(s=r\), \(t=\varDelta _X\), while for a full description of \(L_Q\cdot L_R\), we need to use Theorem 3.8. Specifically, for \(S\in \mathcal {P}(\mathcal {A}\times X)\), \(U\in \mathcal {P}(\mathcal {B}\times X)\), we have \(S\mathrel {(L_Q\cdot L_R)r} U\) iff S and U satisfy conditions forth and back, where forth is given as follows and back is given symmetrically: Whenever \((l,m)\in R\) and \((l,x)\in S\), then there are \(A\in \mathcal {P}(X)\), \(B\in \mathcal {P}(Z)\) such that \(A\times B\subseteq r\) and \(x\in A\), and moreover (i) for all \((l',m)\in R\), there is \(x'\in A\) such that \((l',x')\in S\), and (ii) for all \((m,p)\in Q\), there is \(z\in B\) such that \((p,z)\in U\).
$$\begin{aligned} L_R=K_R\cap K_{R ^ \circ } ^ \circ . \end{aligned}$$
$$\begin{aligned} K_Q\cdot K_R= K_{Q\cdot R}\quad \text {and}\quad L_Q\cdot L_R\le L_{Q\cdot R}. \end{aligned}$$
A further straightforward way to obtain relational connectors is to pull them back along natural transformations:
Lemma and Definition 3.18
Let \(L:F\rightarrow G\) be a relational connector, and let \(\alpha :F'\Rightarrow F\), \(\beta :G'\Rightarrow G\) be natural transformations. Then we have relational connectors \(L\bullet \alpha :F'\rightarrow G\), \(\beta ^ \circ \bullet L:F\rightarrow G'\) defined on \(r:X\, |\!\!\!\!\rightarrow Y\) by \((L\bullet \alpha )r=Lr\cdot \alpha _X\) and \((\beta ^ \circ \bullet L)r= (\beta _Y) ^ \circ \cdot Lr\), respectively.
In particular, from \(\alpha :F\rightarrow G\), we always obtain a relational connector \(\alpha \bullet \textsf{Id}^\textsf{c}_{G}:F\rightarrow G\), which plays a distinguished role:
Definition 3.19
A relational connector \(L:F\rightarrow G\) extends a natural transformation \(\alpha :F\rightarrow G\) if \(\alpha _X\le L\varDelta _X\) for all X.
(In particular, \(L:F\rightarrow F\) extends F iff L extends \( id _F\).)
Theorem 3.20
Let \(\alpha :F\rightarrow G\) be a natural transformation. The relational connector \(\textsf{Id}^\textsf{c}_{G}\bullet \alpha \) is the least relational connector that extends \(\alpha \). In particular, \(\textsf{Id}^\textsf{c}_{G}\) is the least relational connector that extends G.
Example 3.21
We have a variant \(L_{\textsf{f}}\) of the Barr extension of the functor \(F=\mathcal {P}(\mathcal {A}\times (-))\) modelling \(\mathcal {A}\)-LTS (Example 2.1) given by including only the forth condition: For \(r:X\, |\!\!\!\!\rightarrow Y\), \(S\in FX\), \(T\in FY\), we put \(S\mathrel {L_{\textsf{f}}r} T\) iff for all \((l,x)\in S\), there is \((l,y)\in T\) such that \(x\mathrel {r} y\). Now let \(\iota :\mathcal {A}\times (-)\Rightarrow F\) be the inclusion natural transformation. Then we have a relational connector \(L_{\textsf{t}}=L_{\textsf{f}}\bullet \iota :\mathcal {A}\times (-)\rightarrow F\); explicitly, for \(r:X\, |\!\!\!\!\rightarrow Y\), \((l,x)\in \mathcal {A}\times X\), and \(T\in FY\), we have \((l,x)\mathrel {L_{\textsf{t}}r}T\) iff there exists \((l,y)\in T\) such that \(x\mathrel {r}y\). By itself, \(L_{\textsf{t}}\) is not yet very interesting, but we can build further relational connectors using the constructions introduced above; for instance, we have a relational connector \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ :F\rightarrow F\), described by \(S\mathrel {(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ )r} T\) iff there exist \((a,x)\in S\), \((a,y)\in T\) such that \(x\mathrel {r}y\); this connector is symmetric and extends F but fails to be transitive, hence is not a lax extension. We will later employ \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ \) to relate LTS that share an infinite trace (Example 4.8).
Example 3.22
Consider again the functors \(F=\mathcal {P}(\mathcal {A}\times (-))\) and \(G=\mathcal {P}(\mathcal {B}\times (-))\) together with a fixed relation on labels \(R \subseteq \mathcal {A}\times \mathcal {B}\). Note that, for every set X, the elements of FX and GX can be interpreted as relations \(\mathcal {A}\, |\!\!\!\!\rightarrow X\) and \(\mathcal {B}\, |\!\!\!\!\rightarrow X\), respectively. Define the natural transformation \(\alpha :F \Rightarrow G\) by \(\alpha _X(S) = S \cdot R ^ \circ \). Let \(L_{\textsf{f}}^G :G \rightarrow G\) be the ‘forth’ relational connector from Example 3.21 instantiated to G, and consider the relational connector \(L_{\textsf{f}}^G \bullet \alpha \). For \(S \in FX\), \(T \in GY\) and \(r :X\, |\!\!\!\!\rightarrow Y\), we have \(S \mathrel {(L_{\textsf{f}}^G \bullet \alpha ) r} T\) iff \((S \cdot R ^ \circ ) \mathrel {L_{\textsf{f}}^G r} T\). Explicitly, the latter means that if \((l,m) \in R\) and \((l, x) \in S\), then there is \(y \in Y\) such that \((m,y) \in T\) and \(x\mathrel {r} y\). This coincides with the relational connector \(K_R\) from Example 3.17, which is hence induced by a natural transformation and a lax extension. (It does not seem to be the case that \(L_R\) as per Example 3.2/Example 3.17 is induced in this way.)
We can instead compose with a natural transformation on the other side. Let \(\beta :G \Rightarrow F\) be given by \(\beta _X(T) = T \cdot R\), and let \(L_{\textsf{f}}^F :G \rightarrow G\) be the connector \(L_{\textsf{f}}^F\) from Example 3.21, instantiated to F. The connector \(\beta ^ \circ \bullet L_{\textsf{f}}^F :F \rightarrow G\) is given, for \(S \in FX\), \(T \in GY\) and \(r :X\, |\!\!\!\!\rightarrow Y\), by \(S \mathrel {(\beta ^ \circ \bullet L_{\textsf{f}}^F) r} T\) iff \(S \mathrel {L_{\textsf{f}}^F r} (T \cdot R)\). Hence,which differs from \(K_R\) in that here, the quantification over R is existential.
$$\begin{aligned} S \mathrel {(\beta ^ \circ \bullet L_{\textsf{f}}^F) r} T \iff \forall (l,x) \in S. \; \exists (l,m)\in R. \; (m,y) \in T\text { and } x\mathrel {r}y, \end{aligned}$$
Remark 3.23
Analogously to the fact that lax extensions of a functor F are equivalent to certain liftings of F to the category of preordered sets [13], relational connectors \(F\rightarrow G\) can be identified with certain liftings of \(F \times G :\textsf{Set}^2 \rightarrow \textsf{Set}^2\) to the category of binary relations and relation-preserving pairs of functions. Indeed, this category is a fibration over \(\textsf{Set}^2\), and the relational connectors are precisely the liftings that preserve cartesian morphisms; a condition that has featured in situations where liftings of a functor F are used to derive notions of “behavioural conformance” for F-coalgebras (e.g. [3, 11, 18, 45]).
3.3 Lax Extensions as Relational Connectors
For context, we briefly discuss how the additional properties of lax extensions are phrased in terms of the constructions from Section 3, and in particular how lax extensions relate to identity relational connectors.
Definition 3.24
A relational connector \(L:F\rightarrow F\) is transitive if \(L\cdot L\le L\), and symmetric if \(L ^ \circ \le L\). Moreover, L extends F if \(\varDelta _{FX}\subseteq L\varDelta _X\) for all X.
The following observations are straightforward.
Lemma 3.25
Let \(L:F\rightarrow F\) be a relational connector. Then L is symmetric iff \(L ^ \circ = L\) iff \(L\le L ^ \circ \).
Lemma 3.26
Let \(L:F\rightarrow F\) be a relational connector. Then the following hold.
1.
L satisfies condition (L2) in the definition of lax extension iff L is transitive.
2.
L satisfies condition (L3) in the definition of lax extension iff L extends F.
3.
L preserves converse iff L is symmetric.
4.
L is a lax extension of F iff L is transitive and extends F.
5.
If L extends F, then \(L\subseteq L\cdot L\).
6.
If L is a lax extension, then L is idempotent, i.e. \(L\cdot L=L\).
Since lax extensions satisfy naturality, this implies
Theorem 3.27
The lax extensions of a set functor F are precisely the transitive relational connectors that extend F.
As indicated above, a special role is played by identity relational connectors:
Theorem 3.28
Let F be a set functor. Then, \(\textsf{Id}^\textsf{c}_{F}\) is a symmetric lax extension of F. Moreover, F has a diagonal-preserving lax extension iff \(\textsf{Id}^\textsf{c}_{F}\) preserves diagonals.
Proof (sketch)
Most subclaims are obvious by Lemma 3.26 and (3.3). To see that \(\textsf{Id}^\textsf{c}_{F}\) is symmetric, show that \((\textsf{Id}^\textsf{c}_{F}) ^ \circ \) is a right identity: For \(L:F\rightarrow G\), we have \(L\cdot (\textsf{Id}^\textsf{c}_{F}) ^ \circ =(\textsf{Id}^\textsf{c}_{F}\cdot L ^ \circ ) ^ \circ =(L ^ \circ ) ^ \circ =L\) (using Lemma 3.15). \(\square \)
In connection with Theorem 3.20, we obtain moreover:
Corollary 3.29
The identity relational connector \(\textsf{Id}^\textsf{c}_{F}\) is both the smallest lax extension and the smallest symmetric lax extension of a set functor F.
Example 3.30
If F preserves weak pullbacks, then \(\textsf{Id}^\textsf{c}_{F}\) is the Barr extension of F (cf. Remark 2.2); this is immediate from Theorem 3.28, as one shows easily that the Barr extension is below every converse-preserving lax extension. For instance, the standard Egli-Milner lifting is an identity relational connector.
4 Heterogeneous (Bi)simulations
We proceed to introduce a notion of heterogeneous (bi)simulations relating systems of different type; we induce such notions from relational connectors.
Definition 4.1
Let \(L:F\rightarrow G\) be a relational connector. A relation \(r:C\, |\!\!\!\!\rightarrow D\) is an L-simulation between an F-coalgebra \((C,\gamma )\) and a G-coalgebra \((D,\delta )\) ifin pointfree notation, this means that \(r\subseteq \delta ^ \circ \cdot Lr\cdot \gamma \), equivalently \(\delta \cdot r\subseteq Lr\cdot \gamma \). States \(x\in C\), \(y\in D\) are L-similar if there exists an L-simulation r such that \(x\mathrel {r}y\), in which case we write \(x\preceq _Ly\). Occasionally, we will designate the ambient coalgebras C, D explicitly by writing \(x\preceq _L^{C,D}y\); thus, \(\preceq _L^{C,D}\) is a relation \(C\, |\!\!\!\!\rightarrow D\).
$$\begin{aligned} \text {whenever }x\mathrel {r}y,\text { then }\gamma (x)\mathrel {Lr}\delta (y); \end{aligned}$$
In case \(F=G\), r is an L-bisimulation if r and \(r ^ \circ \) are L-simulations. Correspondingly, states \(x\in C\), \(y\in D\) are L-bisimilar if there exists an L-bisimulation r such that \(x\mathrel {r}y\), in which case we write \(x\simeq _Ly\) or, more explicitly, \(x\simeq _L^{C,D}y\).
We note that in case L is a lax extension, these definitions match existing terminology (e.g. [30]). Monotonicity of relational connectors ensures that by the Knaster-Tarski theorem, \(\preceq _L\) is the greatest fixpoint of the map taking r to \(\delta ^ \circ \cdot Lr\cdot \gamma \), and in particular is itself an L-simulation, correspondingly for \(\simeq _L\). We note that L-similarity is invariant under coalgebra morphisms (Section 2), a key fact that hinges on monotonicity and naturality of relational connectors, lending further support to our choice of axiomatics:
Lemma 4.2
Let \(L:F\rightarrow G\) be a connector, let \(r:C\, |\!\!\!\!\rightarrow D\) be an L-simulation between an F-coalgebra \((C,\gamma )\) and a G-coalgebra \((D,\delta )\), and let \(f:(C',\gamma ')\rightarrow (C,\gamma )\), \(g:(C,\gamma )\rightarrow (C'',\gamma '')\) be F-coalgebra morphisms. Then \(r\cdot f\) and \(r\cdot g ^ \circ \) are L-simulations. Symmetric properties hold for G-coalgebra morphisms. Thus, L-similarity is closed under behavioural equivalence (Section 2) on both sides.
Notions of (bi)simulation interact well with composition and converse of relational connectors:
Lemma 4.3
(Composites of simulations). Let \(K:F\rightarrow G\) and \(L:G\rightarrow H\) be relational connectors, and let \((C,\gamma )\) be an F-coalgebra, \((D,\delta )\) a G-coalgebra, and \((E,\varepsilon )\) an H-coalgebra. Then the composite \(s\cdot r:C\, |\!\!\!\!\rightarrow E\) of a K-simulation \(r:C\, |\!\!\!\!\rightarrow D\) and an L-simulation \(s:D\, |\!\!\!\!\rightarrow E\) is an \(L\cdot K\)-simulation. Thus,
$$\begin{aligned} \preceq ^{D,E}_L\cdot \preceq ^{C,D}_K\;\,\subseteq \;\,\preceq ^{C,E}_{L\cdot K} \quad \text {and (if F=G)}\quad \simeq ^{D,E}_L\cdot \simeq ^{C,D}_K\;\,\subseteq \;\,\simeq ^{C,E}_{L\cdot K}. \end{aligned}$$
Lemma 4.4
(Converses of simulations). Let \(L:F\rightarrow G\) be a relational connector, let \((C,\gamma )\) be an F-coalgebra, and let \((D,\delta )\) be a G-coalgebra. If \(r:C\, |\!\!\!\!\rightarrow D\) is an L-simulation, then \(r ^ \circ :D\, |\!\!\!\!\rightarrow C\) is an \(L ^ \circ \)-simulation. Thus,
$$\begin{aligned} \preceq ^{C,D}_{L ^ \circ }\;\,=\;\,(\preceq ^{D,C}_L) ^ \circ \quad \text {and (if F=G)}\quad \simeq ^{C,D}_{L ^ \circ }\;\,=\;\,(\simeq ^{D,C}_L) ^ \circ \end{aligned}$$
It follows that notions of (bi)similarity inherit properties expressed in terms of converse and composition from the inducing lax extensions; for instance:
Lemma 4.5
Let \(L:F\rightarrow F\) be a relational connector. Then the following hold.
1.
If L is transitive, then \(\preceq _L\) and \(\simeq _L\) are transitive.
2.
If L is symmetric, then \(\simeq _L\) is symmetric. Moreover, every L-simulation is an L-bisimulation, so \(\preceq _L\;\,=\;\,\simeq _L\).
3.
If L extends F, then \(\preceq _L\) and \(\simeq _L\) are reflexive.
As a further immediate consequence of Lemma 4.3 and Lemma 4.4, we have the following criterion for preservation of (bi)similarity under relational connectors:
Theorem 4.6
(Transfer of bisimilarity). Let \(K:F\rightarrow F\), \(L:F\rightarrow G\), \(H:G\rightarrow G\) be relational connectors such that \(L\cdot K\cdot L ^ \circ \le H\). Then \(\preceq _L\cdot \preceq _K\cdot \preceq _L ^ \circ \;\,\subseteq \;\, \preceq _H\) and \(\simeq _L\cdot \simeq _K\cdot \simeq _L ^ \circ \;\,\subseteq \;\, \simeq _H\).
Example 4.7
(Transfer of bisimilarity between LTS of different type). Recall the relational connector \(L_R:\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {B}\times (-))\) induced from a relation \(R:\mathcal {A}\, |\!\!\!\!\rightarrow \mathcal {B}\) as per Example 3.2. We note that \( L_{R ^ \circ }=(L_R) ^ \circ . \) This implies that for every L-simulation r, \(r ^ \circ \) is an \(L_{R ^ \circ }\)-simulation, so we suggestively write \(\simeq _R\) for \(\preceq _{L_R}\) and speak of \(L_R\)-bisimilarity.
Recall that the usual notion of bisimilarity on LTS is captured by the identity relational connectors on F and G, respectively (Example 2.1, Example 3.30). It is straightforward to check that if R is right total, thenso that by Theorem 4.6, \(\simeq _R\) transfers bisimilarity from F-coalgebras to G-coalgebras. In elementwise notation, this is phrased as follows: Let \(c,c'\) be states in an F-coalgebra C, and let \(d,d'\) be states in a G-coalgebra D such that \(c'\simeq _R d'\), \(c\simeq _Rd\), and \(c\simeq _F c'\). Then \(d\simeq _G d'\). Similarly, if R is left total, then \(\simeq _R\) transfers bisimilarity from G-coalgebras to F-coalgebras, so of course if R is left and right total, then it transfers bisimilarity in both directions. A similar principle is under the hood of the proof of the operational equivalence of the standard \(\lambda \)-calculus and a variable-free variant called the algebraic \(\lambda \)-calculus in recent work on higher-order mathematical operational semantics [15].
$$\begin{aligned} L_R\cdot id _F\cdot L_R ^ \circ = L_R\cdot L_R ^ \circ \le id _G, \end{aligned}$$
Example 4.8
(Shared traces). Recall the symmetric relational connector \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ :F\rightarrow F\) from Example 3.21, where \(F=\mathcal {P}(\mathcal {A}\times (-))\) is the functor modelling \(\mathcal {A}\)-LTS. States x, y in \(\mathcal {A}\)-LTS are \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ \)-bisimilar iff x and y have a common infinite trace. We may view x as specifying a set of bad infinite traces; then x and y are not \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ \)-bisimilar iff y does not have a bad infinite trace.
Example 4.9
(Weak simulation). Let \(\mathcal {A}\) be a set of labels, with \(\tau \in \mathcal {A}\) a distinguished label for “internal” steps. Let \(\mathcal {A}^*\) be the set of words over \(\mathcal {A}\), with the empty word denoted by \(\varepsilon \), \(F = \mathcal {P}(\mathcal {A}\times (-))\) and \(G = \mathcal {P}(\mathcal {A}^* \times (-))\). We define a relational connector \(L :F \rightarrow G\) by instantiating (the second half of) Example 3.22 to \(R \subseteq \mathcal {A}\times \mathcal {A}^*\) given by \(R = \{(l, \tau ^i l \tau ^j) \mid l \in \mathcal {A}, i,j \ge 0\} \cup \{(\tau , \varepsilon )\}\). In the particular case where the transitions in the G-coalgebra \((D,\delta )\) at hand arise by composing transitions from an F-coalgebra \((D,\delta _0)\), L-simulations from an F-coalgebra \((C,\gamma )\) to \((D,\delta )\) are precisely weak simulations between the \(\mathcal {A}\)-LTS \((C,\gamma )\) and \((D,\delta _0)\).
Example 4.10
(Conformance testing). In model-based testing, a specification is compared to an implementation. Typically, both specifications and implementations are modelled as transition systems, and a given notion of conformance stipulates when an implementation is correct w.r.t. a specification. In the case of the ioco (input/output conformance) relation [43], the specification is an LTS over a set of input and output labels. The implementation is an LTS as well, but is required to be input-enabled, meaning that for every state and every input label there is an outgoing transition with that label. We focus on the deterministic case, which enables a coinductive formulation of ioco conformance [8]. This example has been cast in a general coalgebraic framework [36], in which however the distinction between the type of specification and implementation cannot be made (and in fact, they are assumed to have the same state space).
We write \(X\rightarrow Y\) and \(X \rightharpoonup Y\) for the sets of total and partial functions from X to Y, respectively. We denote the domain of \(f:X \rightharpoonup Y\) by \(\textrm{dom}(f) \subseteq X\), and put \(X \rightharpoonup _{\textrm{ne}}Y=\{f:X \rightharpoonup Y\mid \textrm{dom}(f)\ne \emptyset \}\). Now let I, O be input and output alphabets, respectively. Define the functor F by \(F(X) = (I \rightharpoonup X) \times (O \rightharpoonup _{\textrm{ne}}X)\), and the functor G by \(G(X) = (I \rightarrow X) \times (O \rightharpoonup _{\textrm{ne}}X)\). An F-coalgebra is a suspension automaton, which is non-blocking (there is always at least one output-labelled transition from every state). A G-coalgebra is an input-enabled suspension automaton.
Define \(L :F \rightarrow G\) on \(r :X\, |\!\!\!\!\rightarrow Y\) byThis is a relational connector, and L-simulations capture precisely the ioco-relation on suspension automata, in the coinductive formulation given in [8].
$$\begin{aligned} (\delta _I, \delta _O) \mathrel {L r} (\tau _I, \tau _O) \iff \begin{array}{l} \forall i \in \textrm{dom}(\delta _I). \; \delta _I(i)\mathrel {r} \tau _I(i), \quad \text {and} \\ \forall o \in \textrm{dom}(\tau _O). \; o \in \textrm{dom}(\delta _O) \text { and } \delta _O(o)\mathrel {r} \tau _O(o). \\ \end{array} \end{aligned}$$
The composite relational connector \(L ^ \circ \cdot L :F \rightarrow F\) is described as follows:The existential quantification on outputs arises in this factorization due to the non-emptyness of the domain of partial functions \(O \rightharpoonup _{\textrm{ne}}X\). Simulations for this composite relational connector are precisely the ioco compatibility relations between specifications [8], generalized to a coalgebraic setting in [36].
$$\begin{aligned} (\delta _I, \delta _O) \mathrel {(L ^ \circ \cdot L) r} (\delta _I', \delta _O') \iff \begin{array}{l} \forall i \in \textrm{dom}(\delta _I) \cap \textrm{dom}(\delta _I'). \; \delta _I(i)\mathrel {r} \delta _I'(i), \quad \text {and} \\ \exists o \in \textrm{dom}(\delta _I) \cap \textrm{dom}(\delta _I'). \; \delta _O(o)\mathrel {r} \delta _O'(o). \\ \end{array} \end{aligned}$$
5 Kantorovich Relational Connectors
We next present a construction of relational connectors from relations between modalities for the given functors; in honour of the formal analogy with the classical Kantorovich metric and its coalgebraic generalizations [3, 41, 47], we refer to the arising connectors as Kantorovich relational connectors.
In this context, modalities are understood as induced by predicate liftings in the style of coalgebraic logic [33, 38], and indeed we use the terms modality and predicate lifting interchangeably. Recall that an n-ary predicate lifting for a functor F is a natural transformation \(\lambda \) with components(or just \(\lambda \)) where \(2^{(-)}\) denotes the contravariant powerset functor; that is, \(2^X\) is the powerset of a set X, and \(2^f:2^Y\rightarrow 2^X\) takes preimages under a map \(f:X\rightarrow Y\). The naturality condition thus says explicitly that, for \(a\in FX\) \(f:X\rightarrow Y\), and \(A_1,\dots ,A_n\in 2^Y\), we have \(Ff(a)\in \lambda _Y(A_1,\dots ,A_n)\) iff \(a\in \lambda _X(f^{-1}[A_1],\dots ,f^{-1}[A_n])\). We say that \(\lambda \) is monotone if \(\lambda (A_1,\dots ,A_n)\subseteq \lambda (B_1,\dots ,B_n)\) whenever \(A_i\subseteq B_i\) for \(i=1,\dots ,n\). The dual \(\overline{\lambda }\) of \(\lambda \) is the predicate lifting defined by \(\overline{\lambda }_X(A_1,\dots ,A_n)=FX\setminus \lambda _X(X\setminus A_1,\dots ,X\setminus A_n)\).
$$\begin{aligned} \lambda _X:(2^X)^n\rightarrow 2^{FX} \end{aligned}$$
In logical syntax, we abuse \(\lambda \) as an n-ary modality: If \(\phi _1,\dots ,\phi _n\) are formulae in some modal logic equipped with a satisfaction relation \(\models \) between states in F-coalgebras and formulae, with extensions \({[\![\phi _i]\!]}=\{x\in C\mid x\models \phi _i\}\in 2^C\) in a given F-coalgebra \((C,\gamma )\), then the semantics of the modalized formula \(\lambda (\phi _1,\dots ,\phi _n)\) is given by \(x\models \lambda (\phi _1,\dots ,\phi _n)\) iff \(\gamma (x)\in \lambda _C({[\![\phi _1]\!]},\dots ,{[\![\phi _n]\!]})\). For instance, the unary predicate lifting \(\lozenge \) for the powerset functor \(\mathcal {P}\) given by \(\lozenge _X(A)=\{S\in \mathcal {P}(X)\mid S\cap A\ne \emptyset \}\) captures precisely the usual diamond modality on Kripke frames (‘there exists some successor such that’).
A set \(\varLambda \) of monotone predicate liftings for F induces a lax extension \(L_\varLambda \) of F defined for \(r:X\, |\!\!\!\!\rightarrow Y\), \(a\in FX\), and \(b\in FY\) by \(a\mathrel {L_\varLambda r}b\) iff whenever \(a\in \lambda _X(A_1,\dots ,A_n)\) for n-ary \(\lambda \in \varLambda \) and \(A_1,\dots ,A_n\), then \(b\in \lambda _Y(r[A_1],\dots ,r[A_n])\) (cf. [16, 29, 30]). We show that more generally, one can induce relational connectors from relations between predicate liftings:
Definition 5.1
(Kantorovich connectors). For a functor F, we write \(\textsf{PL}(F)\) for the set of monotone predicate liftings for F. Now let F, G be functors, and let \(\varLambda \) be a relation \(\varLambda :\textsf{PL}(F)\, |\!\!\!\!\rightarrow \textsf{PL}(G)\) that preserves arity; that is, if \((\lambda ,\mu )\in \varLambda \), then \(\lambda \) and \(\mu \) have the same arity, which we then view as the arity of \((\lambda ,\mu )\). We define a relational connector \(L_\varLambda :F\rightarrow G\) for \(r:X\, |\!\!\!\!\rightarrow Y\), \(a\in FX\), and \(b\in GY\) by \(a\mathrel {L_\varLambda r}b\) iff whenever \((\lambda ,\mu )\in \varLambda \) is n-ary and \(A_1,\dots ,A_n\in 2^X\), thenWe briefly refer to \(L_\varLambda \)-similarity as \(\varLambda \)-similarity, and write \(\preceq _\varLambda \) for \(\preceq _{L_\varLambda }\). A relational connector L is Kantorovich if it has the form \(L=L_\varLambda \) for a suitable \(\varLambda \) as above. We write \(\overline{\varLambda }=\{(\overline{\lambda },\overline{\mu })\mid (\lambda ,\mu )\in \varLambda \}\).
$$\begin{aligned} a\in \lambda _X(A_1,\dots ,A_n)\quad \text {implies} \quad b\in \mu _Y(r[A_1],\dots ,r[A_n]). \end{aligned}$$
Theorem 5.2
Under Definition 5.1, \(L_\varLambda \) is indeed a relational connector.
Example 5.3
1.
For every \(l\in \mathcal {A}\), we have a predicate lifting \(\lozenge _l\) for \(\mathcal {P}(\mathcal {A}\times (-))\) given by \(\lozenge _l(A)=\{S\in \mathcal {P}(\mathcal {A}\times X)\mid \exists x\in A.\,(l,x)\in S\}\). The arising modality is the usual diamond modality of Hennessy-Milner logic, and the dual of \(\lozenge _l\) is the usual box modality \(\square _l\). The connectors \(K_R,L_R:\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {B}\times (-))\) from Example 3.17 are Kantorovich: We have \(K_R=L_\varLambda \) and \(L_R=L_{\varLambda \cup \overline{\varLambda }}\) for \(\varLambda =\{(\lozenge _l,\lozenge _m)\mid (l,m)\in R\}\).
2.
We can restrict the predicate lifting \(\lozenge _l\) from the previous item to a predicate lifting \(\lozenge _l\) for \(\mathcal {A}\times (-)\) (so \(\lozenge _l(A)=\{(l,x)\mid x\in A\}\)). The relational connector \(L_{\textsf{t}}=L_{\textsf{f}}\bullet \iota :\mathcal {A}\times (-)\rightarrow \mathcal {P}(\mathcal {A}\times (-))\) from Example 3.21 is Kantorovich for \(\varLambda =\{(\lozenge _l,\lozenge _l)\mid l\in \mathcal {A}\}\). We will later give a Kantorovich description of the composite connector \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ \) (Example 5.7).
3.
Given a label \(l \in \mathcal {A}\), define the predicate lifting \(\lozenge _l\) for \(\mathcal {A}\rightharpoonup (-)\) by \(\lozenge _l(A) = \{\delta :\mathcal {A}\rightharpoonup X \mid l \in \textrm{dom}(\delta ) \text { and } \delta (l) \in A\}\) for \(A\in 2^X\). Its dual is given by \(\square _l(A) = \{\delta \mid l \in \textrm{dom}(\delta ) \text { implies } \delta (l) \in A\}\). Further, we define a 0-ary modality \({\downarrow _l} = \{\delta \mid l \not \in \textrm{dom}(\delta )\}\). These modalities allow us to capture the ioco connector \(L :F \rightarrow G\) from Example 4.10. First, assuming that I and O are disjoint, the modalities \(\lozenge _l, \square _l, \downarrow _l\) for \(i \in I \cup O\) can be extended to F and G in the obvious way by projection (and they are extended to total functions and partial functions with a non-empty domain without change). Now, L is Kantorovich for \(\varLambda = \{(\lozenge _i, \lozenge _i) \mid i \in I\} \cup \{(\square _o, \square _o) \mid o \in O\} \cup \{({\downarrow _o}, {\downarrow _o}) \mid o \in O\}\).
4.
Given \(\epsilon \in [0,1]\), we have predicate liftings \(L_{\epsilon ,l}\) (for \(l\in \mathcal {A}\)) for the functor \(\mathcal {D}(\mathcal {A}\times (-))\) modelling probabilistic LTS, given by \(L_{\epsilon ,l}(A)=\{\alpha \in \mathcal {D}(\mathcal {A}\times X)\mid \alpha (\{l\}\times A)\ge \epsilon \}\) for \(A\in 2^X\). Putting \(\varLambda =\{(\lozenge _l,L_{\epsilon ,l})\mid l\in \mathcal {A}\}\), we obtain relational connectors \(L_\varLambda ,L_{\overline{\varLambda }},L_{\varLambda \cup \overline{\varLambda }}:\mathcal {P}(A\times (-))\rightarrow \mathcal {D}(\mathcal {A}\times (-))\). Explicitly, for \(r:X\, |\!\!\!\!\rightarrow Y\), \(S\in \mathcal {P}(\mathcal {A}\times X)\), and \(\alpha \in \mathcal {D}(\mathcal {A}\times Y)\), we have (i) \(S\mathrel {L_\varLambda r}\alpha \) iff whenever \((l,x)\in S\), then \(\alpha (\{l\}\times r[\{x\}])\ge \epsilon \) ; (ii) \(S\mathrel {L_{\overline{\varLambda }}\,r}\alpha \) iff whenever \(\alpha (\{l\}\times B)\ge \epsilon \), then there are \((l,x)\in S\) and \(y\in B\) such that \(x\mathrel {r}y\); and (iii) \(S\mathrel {L_{\varLambda \cup \overline{\varLambda }}\,r}\alpha \) iff both (i) and (ii) hold. Roughly speaking, similarity w.r.t. these connectors between an \(\mathcal {A}\)-LTS C and probabilistic \(\mathcal {A}\)-LTS D specifies what may happen in D with non-negligible probability, where \(\epsilon \) specifies the negligibility threshold. For instance, an \(L_\varLambda \)-simulation \(r:C\rightarrow D\) witnesses that behaviour embodied in C is enabled with non-negligible probability in D, while an \(L_{\overline{\varLambda }}\)-simulation \(r:C\rightarrow D\) witnesses that things that can happen with non-negligible probability in D are foreseen in C.
We record basic facts on the interaction of the Kantorovich construction with composition and converse of relational connectors:
Theorem 5.4
Let \(\varLambda :\textsf{PL}(F)\, |\!\!\!\!\rightarrow \textsf{PL}(G)\) and \(\varTheta :\textsf{PL}(G)\, |\!\!\!\!\rightarrow \textsf{PL}(H)\). Then
1.
\(L_\varTheta \cdot L_\varLambda \le L_{\varTheta \cdot \varLambda }\)
2.
\((L_\varLambda ) ^ \circ =L_{(\overline{\varLambda }) ^ \circ }\).
(Recall that \(\overline{\varLambda }\) dualizes all modalities.) Specializing to relational connectors \(F\rightarrow F\), we thus recover the standard way of inducing lax extensions from predicate liftings [14, 30] as described above:
Corollary 5.5
Let F be a functor, and let \(\varLambda :\textsf{PL}(F)\, |\!\!\!\!\rightarrow \textsf{PL}(F)\).
1.
If \(\varLambda \cdot \varLambda \subseteq \varLambda \), then \(L_\varLambda \) is transitive.
2.
If \(\varLambda \) is closed under duals, i.e. \(\overline{\varLambda }\subseteq \varLambda \) (equivalently \(\overline{\varLambda }=\varLambda \)), and symmetric, then \(L_\varLambda \) is symmetric.
3.
If \(\varLambda \subseteq id \), then \(L_\varLambda \) is a lax extension of F.
4.
If \(\varLambda \subseteq id \) and the set \(\{\lambda \mid (\lambda ,\lambda )\in \varLambda \}\) of predicate liftings is separating, then \(L_\varLambda \) is a normal lax extension of F.
Remark 5.6
(Composing Kantororovich connectors). The upper bound \(L_\varTheta \cdot L_\varLambda \le L_{\varTheta \cdot \varLambda }\) on composites of Kantorovich connectors \(L_\varTheta , L_\varLambda \) given in Example 5.4 is not always tight. In the simple case of the connectors \(K_R:\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {B}\times (-))\) induced by relations \(R:\mathcal {A}\, |\!\!\!\!\rightarrow \mathcal {B}\) (Examples 3.17 and 5.3), we do indeed have exact equality (Example 3.17). For the general case, one can improve the upper bound (by including more pairs of modalities) in at least two ways. First, in the composite \(\varTheta \cdot \varLambda \) of the relations \(\varLambda :\textsf{PL}(F)\, |\!\!\!\!\rightarrow \textsf{PL}(G)\) and \(\varTheta :\textsf{PL}(G)\, |\!\!\!\!\rightarrow \textsf{PL}(H)\), one can include weakening in the middle step. Formally, we write \(\le \) for the pointwise inclusion order on predicate liftings, and put \(\varTheta \mathbin {\blacktriangleright }\varLambda =\{(\lambda ,\pi )\mid \exists (\lambda ,\mu )\in \varLambda ,(\mu ',\pi )\in \varTheta \mid \mu \le \mu '\}\). Then \(L_\varTheta \cdot L_\varLambda \le L_{\varTheta \mathbin {\blacktriangleright }\varLambda }\). Moreover, monotone predicate liftings are closed under taking positive Boolean combinations both above and below; e.g. if \(\lambda \) and \(\mu \) are unary monotone predicate liftings, then the transformation \(\pi \) taking predicates A, B to \(\lambda (A\vee B)\wedge \mu (A\wedge B)\) is a binary monotone predicate lifting. We write \(\varLambda ^\textsf{pos}\) for the closure of \(\varLambda \) under componentwise positive Boolean combinations in this sense; e.g. if \((\lambda _1,\lambda _2),(\mu _1,\mu _2)\in \varLambda \), then \((\pi _1,\pi _2)\in \varLambda ^\textsf{pos}\) where \(\pi _i(A,B)=\lambda _i(A\vee B)\wedge \mu _i(A\wedge B)\). One checks easily that \(L_\varLambda =L_{\varLambda ^\textsf{pos}}\), so overall we haveWe next give an example where one actually has equality; we leave it as an open problem whether equality holds in general.
$$\begin{aligned} L_\varTheta \cdot L_\varLambda \le L_{\varTheta ^\textsf{pos}\,\mathbin {\blacktriangleright }\varLambda ^\textsf{pos}}. \end{aligned}$$
(5.1)
Example 5.7
Recall from Example 5.3.2 that the connector \(L_{\textsf{t}}:\mathcal {A}\times (-)\rightarrow \mathcal {P}(\mathcal {A}\times (-))\) equals \(L_\varLambda \) where \(\varLambda =\{(\lozenge _l,\lozenge _l)\mid l\in \mathcal {A}\}\); thus, \(L_{\textsf{t}} ^ \circ =L_{(\overline{\varLambda }) ^ \circ }\) by Theorem 5.4. Assume for simplicity that \(\mathcal {A}\) is finite. Note that we havewhere \(\bigwedge _{l\in \mathcal {A}}\square _l(-)_l\) takes an \(\mathcal {A}\)-indexed family of predicates \(A_l\) to \(\bigcap _{l\in \mathcal {A}}\square _lA_l\), correspondingly for \(\bigvee _{l\in \mathcal {A}}\lozenge _l(-)_l\), since this pair represents a valid implication over \(\mathcal {A}\times (-)\). From this observation, one easily concludes that \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ =L_\varLambda \cdot L_{(\overline{\varLambda }) ^ \circ }=L_{\varLambda ^{\textsf{pos}}\mathbin {\blacktriangleright }(\overline{\varLambda }^{\,\textsf{pos}}) ^ \circ }\), i.e. we have equality in the applicable instance of (5.1). We will use this fact to obtain a logical characterization of \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ \)-bisimilarity (i.e. of sharing an infinite trace) in Example 6.5.
$$\begin{aligned}\textstyle (\bigwedge _{l\in \mathcal {A}}\square _l(-)_l,\bigvee _{l\in \mathcal {A}}\lozenge _l(-)_l)\in \varLambda ^{\textsf{pos}}\mathbin {\blacktriangleright }(\overline{\varLambda }^{\,\textsf{pos}}) ^ \circ , \end{aligned}$$
6 Expressiveness
We now go on to establish an expressiveness theorem in the style of the classical Hennessy-Milner theorem, which states that two states in finitely branching LTS are bisimilar iff they satisfy the same formulae of Hennessy-Milner logic. Our present version subsumes the classical theorem and coalgebraic generalizations, but also variants for asymmetric comparisons such as simulation, and hence instead works with forward preservation of formula satisfaction in a logic with only positive Boolean combinations, introduced next:
Definition 6.1
Let \(\varLambda :\textsf{PL}(F)\, |\!\!\!\!\rightarrow \textsf{PL}(G)\). Then the set \(\mathcal {F}(\varLambda )\) of \(\varLambda \)-formulae \(\phi ,\psi \) is given by the grammarWe interpret \(\varLambda \)-formulae over both F-coalgebras and G-coalgebras. For a state x in an F-coalgebra \((C,\gamma )\) and a \(\varLambda \)-formula \(\phi \), we write \(x\models _F\phi \), or just \(x\models \phi \), to indicate that x satisfies \(\phi \); similarly, we write \(y\models _G\phi \) or just \(y\models \phi \) to indicate that a state y in a G-coalgebra \((D,\delta )\) satisfies \(\phi \). We denote the extension of \(\phi \) in C by \({[\![\phi ]\!]}_C=\{x\in C\mid x\models C\}\), similarly for D. The satisfaction relations are then defined by the usual clauses for the Boolean operators, and byWe refer to the modal logic thus defined as \(\mathcal {L}(\varLambda )\).
$$\begin{aligned} \mathcal {F}(\varLambda )\ni \phi ,\psi :\,\!:=\bot \mid \top \mid \phi \wedge \psi \mid \phi \vee \psi \mid \langle \lambda ,\mu \rangle \phi \qquad ((\lambda ,\mu )\in \varLambda ). \end{aligned}$$
$$\begin{aligned} x\models _F\langle \lambda ,\mu \rangle \phi \text { iff } \gamma (x)\in \lambda ({[\![\phi ]\!]}_C),\qquad y\models _G\langle \lambda ,\mu \rangle \phi \text { iff } \delta (y)\in \mu ({[\![\phi ]\!]}_D). \end{aligned}$$
One shows easily that the logic \(\mathcal {L}(\varLambda )\) is preserved under \(L_\varLambda \)-similarity:
Proposition 6.2
Let \(\varLambda :\textsf{PL}(F)\, |\!\!\!\!\rightarrow \textsf{PL}(G)\), and let \(\phi \) be a \(\varLambda \)-formula. Whenever \(x\preceq _\varLambda y\) and \(x\models _F\phi \), then \(y\models _G\phi \).
The converse is less straightforward, and (like the classical Hennessy-Milner theorem) depends on finite branching. For brevity, we say that an F-coalgebra \((C,\gamma )\) is finitely branching if for every \(x\in C\), there exists a finite subset \(C'\subseteq C\) such that \(\gamma (x)\in FC'\subseteq FC\) (cf. assumptions made in Section 2).
Theorem 6.3
(Expressiveness). Let \(\varLambda :\textsf{PL}(F)\, |\!\!\!\!\rightarrow \textsf{PL}(G)\). Then \(\varLambda \)-similarity coincides with theory inclusion in \(\mathcal {L}(\varLambda )\) on finitely branching coalgebras; that is, for states \(x\in C\), \(y\in D\) in finitely branching coalgebras \((C,\gamma :C\rightarrow FC)\) and \((D,\delta :D\rightarrow GD)\), we have \(x\preceq _\varLambda y\) iff for every \(\varLambda \)-formula \(\phi \), whenever \(x\models _F\phi \), then \(y\models _G\phi \).
Proof (sketch)
Show that theory inclusion \(r=\{(x,y)\in C\times D\mid \forall \phi \in \mathcal {F}(\varLambda ).\,x\models _F\phi \implies y\models _G\phi \}\) is an \(L_\varLambda \)-simulation. \(\square \)
Remark 6.4
From Theorem 6.3, we recover in particular the coalgebraic generalization of the Hennessy-Milner theorem for behavioural equivalence [33, 38], restricted to monotone modalities, by instantiating to \(\varLambda \subseteq id \) satisfying the usual separation condition (cf. Corollary 5.5). This theorem applies to a logic with full Boolean propositional base; note here that when \(\varLambda \) is closed under duals, our logic admits an encoding of negation via negation normal forms. Also, Theorem 6.3 subsumes coalgebraic Hennessy-Milner theorems for behavioural preorders such as simulation [23, 46]. Our main interest is in heterogeneous examples, listed next.
Example 6.5
1.
From the Kantorovich description of the relational connectors \(K_R,L_R:\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {B}\times (-))\) induced from \(R:\mathcal {A}\, |\!\!\!\!\rightarrow \mathcal {B}\) (Example 5.3.1), we obtain logical characterizations of \(K_R\)-similarity and \(L_R\)-(bi)similarity on finitely branching \(\mathcal {A}\)-LTS and \(\mathcal {B}\)-LTS. For instance, states \(x\in C\), \(y\in D\) in an \(\mathcal {A}\)-LTS C and a \(\mathcal {B}\)-LTS D, both finitely branching, are \(L_R\)-bisimilar iff x and y satisfy the same formulae in a modal logic with modalities \(\langle \lozenge _l,\lozenge _m\rangle \) and \(\langle \square _l,\square _m\rangle \) for \((l,m)\in R\).
2.
In Example 5.3.3, a Kantorovich description is given for ioco simulation, yielding a logical characterization by Theorem 6.3. The logic features the modalities \(\lozenge _i\) for inputs \(i \in I\), \(\square _o\) for outputs \(o \in O\) and “undefinedness” modalities \(\downarrow _o\), which hold at a state iff there is no outgoing o-transition from that state.
3.
The Kantorovich definition of the relational connector \(L_\varLambda :\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {B}\times (-))\), for \(\varLambda =\{(\lozenge _l,L_{l,\epsilon })\mid l\in \mathcal {A}\}\) as per Example 5.3.4, implies a logical characterization of \(L_\varLambda \)-simulation: Given states \(x\in C\), \(y\in D\) in an finitely branching \(\mathcal {A}\)-LTS C and a finitely branching probabilistic \(\mathcal {A}\)-LTS D, we have \(x\preceq _\varLambda y\) iff whenever x satisfies a formula \(\phi \) in the positive fragment of Hennessy-Milner logic with only diamond modalities \(\lozenge _l\), then y satisfies the probabilistic modal formula obtained from \(\phi \) by replacing \(\lozenge _l\) with \(L_{l,\epsilon }\) throughout. Corresponding characterizations hold for \(L_{\overline{\varLambda }}\)-similarity and \(L_{\varLambda \cup \overline{\varLambda }}\)-similarity.
4.
From the Kantorovich description of the connector \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ :\mathcal {P}(\mathcal {A}\times (-))\rightarrow \mathcal {P}(\mathcal {A}\times (-))\), we obtain a logical characterization of \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ \)-bisimilarity, i.e. of sharing an infinite trace: States x, y in finitely branching \(\mathcal {A}\)-LTS are \(L_{\textsf{t}}\cdot {L_{\textsf{t}}} ^ \circ \)-bisimilar iff whenever x satisfies a formula \(\phi \) in a positive modal logic with \(|\mathcal {A}|\)-ary modalities \(\bigwedge _{l\in \mathcal {A}}\square _l(-)_l\) as per Example 5.7, then y satisfies the formula obtained from \(\phi \) by replacing \(\bigwedge _{l\in \mathcal {A}}\square _l(-)_l\) with \(\bigvee _{l\in \mathcal {A}}\lozenge _l(-)_l\) throughout. We note that in a scenario where we view x as specifying a set of bad traces, this means that the fact that y does not have a bad trace can be witnessed by a single counterexample formula \(\phi \).
7 Conclusions
We have presented a systematic approach to comparing systems of different transition types, abstracted as set functors in the paradigm of universal coalgebra [37]: We induce notions of heterogeneous (bi)simulation from relational connectors among set functors. We have exhibited a number of key constructions of relational connectors, including composition, converse, identity, and a Kantorovich construction in which a connector is induced from a relation between modalities. Building on the latter, we have proved a Hennessy-Milner type theorem that characterizes heterogeneous (bi)similarity in terms of theory inclusion in a flavour of positive coalgebraic modal logic [23] that is interpretable over both of the involved system types. One instance of this result asserts that absence of a shared trace between LTS can be witnessed by a pair of modal formulae in Hennessy-Milner logic.
We leave quite a few problems open for further investigation, maybe most notably including the question whether every relational connector among finitary functors is Kantorovich (this holds for lax extensions [26, 29, 30], which form a special case of relational connectors, and generalizes to arbitrary functors when infinitary modalities are allowed [14, 38]). More specifically, one would be interested in a logical descriptions of composites of Kantorovich connectors, working from Remark 5.6. A further open question is under what conditions similarity for a composite relational connector \(L \cdot K\) equals the composite of the similarity relations for L and K respectively—currently, we only have one inclusion (Lemma 4.3). This is of particular interest for the example on ioco conformance (Example 4.10), where two specifications are known to be compatible iff they have a common conforming implementation [8], a result that has been recovered in a coalgebraic setting [36]. A further issue for future research is to develop the coinductive up-to techniques [7, 35] for relational connectors.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
