Try   HackMD

Cospan Bisimulation 2

(draft references to be added) (up)


Introduction

We collect some results on cospan bisimulations. These results invariable relate ordinary bisimulations on sets with ordered bisimulation on ordered sets. Since bisimulations on ordered sets include simulations as well as bisimulations we will call them (bi)simulations.

Overview

We first review notation and define the notion of an order-extension of a set-functor.

The subsection span and cospan bisimulations investigates the relationship between cospan bisimulations and span bisimulations.

The subsection cospan (bi)simulations and change of base looks at cospan (bi)simulations enriched over different quantales.

Summary

Together this shows that cospan (bi)simulation works uniformly over sets, orders, metric spaces and

Ω-categories. For example, Rutten's final coalgebra theorem for sets can now be seen as a special case of Worrell's final coalgebra theorem for
Ω
-categories.

Questions

If

f and
f
are cospan-bisimulations, is then
f
a coalgebra morphism?

Connections with logic induced bisimulations?

Notation

In this section,

  • Ord
    denotes the category
    Pre
    of preorders or the category
    Pos
    of posets.
  • D:SetOrd
    denotes the discrete functor and we write
    CDV
    for the induced chain of adjoints.
  • T
    denotes a functor
    SetSet
    .

Order-Extensions

Following on from part one, we are interested in preordification

T of
T
. Preordifictions are universal solutions to the problem of finding a
T
together with a transformation
DTTD
. In fact, the preordification
T
of
T
can be defined as the
Ord
-enriched left Kan extension of
DT
along
D
. But some results hold more generally for any ordered extension
DTTD
.

Definition: We call

T:OrdOrd an order-extension of
T:SetSet
if there is a natural transformation
DTTD.

Remark: Equivalently,

T is an order-extension of
T
if there is a natural tranformation
TDTV
. This also captures the intuition that
T
adds ordering to
T
. If one insists on
TDTV
being an iso, this notion is equivalent to the one of Jacobs and Jacobs-Hughes (ADD REFERENCES).

Question:

TDTV iso is equivalent to
DTTD
being bijective. Is there an interesting example of an order-extension for which
DTTD
is not bijective?

Remark: The mate of

DTTD is
TVVT
. If
T
is the preordification then
TVVT
is an iso, but for posetifications this does not need to be the case as the example of convex powerset (=the posetification of powerset) shows. We summarise some of the relationships between properties of these natural transformations in the table below.

1
DTTD
T
' is an order-extension of
T
2
DTTD
iso
T
a strict order-extension of
T
3
T
left Kan extension,
T
is the ordification of
T
4
TVVT
iso
T
' is an order-lifting of
T
5
TVTD
iso
TD
is an order on
T

321 and
25
and
45
. If
Ord=Pre
, then also
34
.

Span and cospan bisimulations

The following result makes precise that every span bisimulation is a cospan (bi)simulation.

Proposition: Let

T be an order-extension of
T
. If two states in two
T
-coalgebras are
T
-span-bisimilar then they are
T
-cospan-(bi)similar.

Proof: Let

XTX and
YTY
be two
T
-caolgebras. Let
XRY
be a
T
-span bisimulation. Let
R
be the cocomma of
XRY
. Applying
T
to the square
DRDXDYR

and using the arrow

RTR from the span-bisimulation the universal property of the cocomma
R
gives the required arroe
RTR
. QED

Examples: A number of familiar examples arise as instances of this proposition.

  • T=P
    and
    T
    the downset or upset or convex powerset functor: Every span-bisimulation is also a cospan-bisimulation. Moreover, if two points are bisimilar then they are forward-similar and backward-similar.
  • T=UpP
    is the monotone neibhbourhood frame functor.
    T
    is its ordification or also
    DU
    or also
    UoDo
    .

Questions: Is there something more one can say about structural relationships between bisimulation and simulation? For example, one could try to isolate those functors for which forward simulation plus backward simulation is bisimulation, but I do not know how interesting this would be (is there a good abstract notion of "deterministic" functor?). Anything else?

For weak pullback preserving functors, we also have the converse of the previous proposition.

Proposition: Let

T:SetSet preserve weak pullbacks. If two states in two
T
-coalgebras are cospan-bisimilar then they are span-bisimilar.

Proof: Let

R be a cospan bisimulation and
XRY
be the collage, hence cocomma, of
R
. Let
T
be the ordification of
T
. With the help of the iso
DTTD
we can consider the
(R,R)
-square as a cocomma in ordered sets. Cocommas are exact. Since ordifications
T
preserve exact squares if
T
preserves weak pullbacks [Theorem 4.11,BKV15] , the
(TR,TR)
-square is exact. But exact squares in posets are weak comma squares, hence there is an
RTR
making
R
into a span bisimulation. QED

Morphisms and Bisimulations

In sets every function is a relation and every coalgebra morphism a bisimulation. In ordered sets every function

f:XY gives rise to two relation
f:XY
and
f:YX
with
(x,y)f  fxy(y,x)f  yfx

Proposition: Let

T:OrdOrd. If
f
is a
T
-coalgebra morphism, then
f
and
f
are cospan-(bi)simulations.

Proof:

f and
f
are the weakening closures of the spans
(id,f)
and
(f,id)
, respectively. Recall the definition of cospan-(bi)simulation and the fact that the collage of the weakening closure of a relation represented by a span
(p,q)
is the cocomma of
(p,q)
. Now the proposition follows from the universal property of cocommas. QED

Example: Recall that

R is a
DU
-cospan-(bi)simulation iff
xRy    aξx.bνy.yb.xa. xRy

We also know that

f:XY is a morphism
(X,ξ)(Y,ν)
of
DU
-coalegbras iff
aξx.bν(fx).yb.xa.fxybν(fx).aξ(x).xa.yb. yfx

It is now easy to check that the first clause says precisely that

f is a (bi)simulation and the second clause that
f
is a (bi)simulation. (I find this very pretty.)

Question: Can we prove the converse of the proposition? - - - This is interesting, I wrote out the obvious diagrams, but I didn't see how to proceed. - - - Maybe the converse is only true in special cases?

Cospan (bi)simulations and change of base

Cospan (bi)simulations allow us to see ordinary coalgebraic bisimulations as well as quantale enriched ones in the same framwork. The basic picture, taken from Section 4 of [BKV19] is as follows.

CDV take, respectively, connected components, discrete preorders and underlying sets. They lift via doctrinal adjunction to coalgebras since the right adjoints satisfy
DTSetTPreD
and
VTPreTSetV
.

Image Not Showing Possible Reasons
  • The image file may be corrupted
  • The server hosting the image is unavailable
  • The image path is incorrect
  • The image format is not supported
Learn More →

On the right-hand side,

d is the top and bottom preserving embedding with a right adjoint
v
and, if
Ω
is non-trivial and integral[1], a left adjoint
c
. The left ajoint
c
maps all elements other than bottom to
1
and the right adjoint
v
maps all elements other than top to
0
. The adjunction
dv
lifts to a
Pre
-enriched adjunction between the categories of coalgebras. If the quantale
Ω
has no zero-divisors, then
c
is a quantale-morphism and
cd
lifts to
Ω
-cat enriched adjunction between categories of coalgebras. See Propositions 4.9 and 4.10 of [BKV19] for details.

Propositions ?? I think, mutatis mutandis, we can move the two propositions above from the left Set/Pre column to the right Pre/

Ω-cat column

Examples ?? Can we make an example of ordinary transition systems and bisimulation and then a metric example? Are there scenarios where one would want an orderd coalgebra as an abstraction of a metric coalgebra? I never really looked so much at Kripke frames over metric spaces any ideas?

References

Balan, Kurz, Velebil: Positive fragments of coalgebraic logics. 2015.

Balan, Kurz, Velebil: Extending set functors to generalised metric spaces. 2019.

Jacobs

Hughes-Jacobs

Further

Scratch notes on exact squares


  1. A quantale is integral if the neutral element of the multiplication is the top element. ↩︎