Ichiro Hasuo

Tracing Anonymity with Coalgebras

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

The ultimate aim• pervasive, important• fail easily•…
• we don’t
don t quite understand them!

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Coalgebras
Good balance:
mathematicalthti lsimplicity((potential)
t ti l)applicability

In this thesis:• more applications are found• further mathematical theory is developedTracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Coalgebras
coalgebraically

FXsystemcoalgebraXbehavior‐
behavior‐
preservingi map

behavior

morphism of
coalgebrasl bby final
coalgebra

FXFfc

XFXc

X

FYdfY

FZ
final
Zb h( )
beh(c)

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Overview
Coalgebraic theory of
traces and simulations(Ch 2(Ch.
2‐3)3)• via coalgebras in a
Kl i li category
Kleisli• apply to both• non‐determinism
non determinism• probability• case study:
probabilistic
anonymity (Ch. 4)

Concurrency incoalgebrasg((Ch. 5))• the microcosm
principle
i i l appears

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

In Sets: bisimilarity
system as coalgebra

behaviorb h i byb final
fi lcoalgebra

FXFXXXc

FZ
final
Zbeh(c)NBh theyh mean exactly
l depends
dd on whichhi h• whatcategory they’re in
X, FX, FZ, …

sets

X ÆY

functionstandard• they are in the category Sets
• “behavior” captures bisimilarity

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Bisimilarity vs.
vs trace semanticsa≠=acb

When do wedecidecb

Tracesemantics

BisimilarityoraAnyway we getÆ?

Æor

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Coalgebraic trace semantics
Behavior by
final coalgebra
FXc

XFZ
finalZbeh(c)

captures…

inSetsGeneric Trace Semantics via
Coinduction
IH, Bart Jacobs & Ana Sokolova
Logical Method in Comp. Sci.
3(4:11), 2007

“Kleisli
Kleisli category”
categoryo a category wherebranching is implicito X Æ Y : “branching function” from X to Yo T : parametert ffor branchingbbranching‐hi ‐typetbisimilarity(standard)≠in( ) traceKl(T)semantics(Ch. 2)=Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Different “branching-types”
branching-types
FXc

X

T=PFZ
finalZbeh(c)trace semantics:aÆba Æcnon‐‐deterministic
nond ti i ti branchingbhiabain Kl(T) captures
trace semantics
T : parameter for
trace‐typesemantics:“branchingbranching‐type”
a Æ b : 1/3
T = D a Æ c : 2/3
b bili ti branchingbhi
probabilistic

acb 11323

a1 c

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Coalgebraic simulations (Ch(Ch. 3)morphism ofcoalgebras
FX

Ffc

X

FY
df

Y

in
Sets

functionalbi i l ti
bisimulation(standard)lax morphism
p= forward
simulationinKl(T)??

oplax
p morphismp
genericity again: both for= backward• T = P (non‐determinism)
simulation• T = D (probability)
Generic Forward and Backward
Simulations
IHProc. CONCUR 2006
LNCS 4137∃ fwd/bwd simulation Î trace inclusion

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

genericity : both for(non determinism)• T = P (non‐determinism)• T = D (probability)

Summary so far

coalgebra

FXin Sets

in Kl(T)systemsystemCh. 3

Xmorphism of coalgebra
FX

Ffc

X

FY

functional bisimilaritydf

forward simulation (lax)backward similation (oplax)

YCh. 2by final coalgebra
FXcXFZ
finalZbeh(c)bisimilarity

trace semantics

theory ofbisimilarity

theory of traces
and simulations

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Probabilistic Anonymity via
Coalgebraic Simulations
IH & Yoshinobu Kawabe
Proc. ESOP 2007
LNCS 4421

Case study:
probabilistic anonymity (Ch. 4)

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuocategory ofcoalgebras
final
coalgebra

Concurrency““concurrency”” , “b“behavior”
h i ”

2 ‐ dimensional , nested algebraic structureTracinng Anony
ymity wiith Coalg
gebraso Hasuo
IchiroConcurrency and themicrocosm principle (Ch. 5)

science ofgenericcomputercompositionality
systemstheorem

The Microcosm Principle andConcurrency in Coalgebra
IH, Bart Jacobs & Ana Sokolova
To appear in Proc. FoSSaCS 2008
LNCS

concurrency,y,compositionality,
behavior, …

formalization of microcosm
principle in 2‐2‐categories
1
⇓XL
CatC

mathematics

Tracinng Anony
ymity wiith Coalg
gebrasIchiroo Hasuo

Summary
Coalgebraic theory oftraces and simulations(Ch 2(Ch.
2‐3)3)• via coalgebras in aKl i li categoryKleisli• apply to both• non‐determinism
non determinism• probability• case study:
probabilistic
anonymity (Ch. 4)

Concurrency incoalgebrasg((Ch. 5))• the microcosm
principle
i i l appears