LICS 1997 Logique LICS 2002

Une théorie des processus probabilistes
continus: équivalence et distanceRichard Blute, Abbas Edalat,Josée Desharnais, Prakash Panangaden,Vineet Gupta, Radha Jagadeesan

Prix test-of-time LICS 2017 et LICS 2020
Bisimulation for Labelled Markov Processes. LICS 1997.
The Metric Analogue of Weak Bisimulation for Probabilistic
Processes. LICS 2002.

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Outline1

LICS 1997

2Logique3

LICS 2002

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Contexte LMPs

Problématique générale – systèmes interactifs
Étant donné un contexte C[·], et sachant qu’une
composante approxime un comportement idéal, peut-on
comparer C[composante] et C[idéal] ?

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Contexte LMPs

Problématique générale – systèmes interactifs
Étant donné un contexte C[·], et sachant qu’une
composante approxime un comportement idéal, peut-on
comparer C[composante] et C[idéal] ?
Substitution sécuritaire : peut-on substituer une
composante dans un programme sans augmenter lapossibilité de perte d’information ?
d(c, c 0 ) <  ⇒ |perte(C[c]) − perte(C[c 0 ])| < δJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Contexte LMPs

Problématique générale – systèmes interactifs
Étant donné un contexte C[·], et sachant qu’une
composante approxime un comportement idéal, peut-on
comparer C[composante] et C[idéal] ?
Substitution sécuritaire : peut-on substituer une
composante dans un programme sans augmenter lapossibilité de perte d’information ?
d(c, c 0 ) <  ⇒ |perte(C[c]) − perte(C[c 0 ])| < δ
Pour analyser des systèmes ayant un nombre d’états infini,non dénombrable, on veut une représentation qui garde
toutes les informations – quite à approximer ou discrétiser
par la suite.
Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Contexte LMPs

D’abord les modéliser/décrire/représenterOn veut modéliser les systèmest0

interactifs, concourantsa

non déterministes

at10

t1

probabilistesbà états possiblement infinist2Josée Desharnais, Université Laval(S, A, −→)

c

t20

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Contexte LMPs

D’abord les modéliser/décrire/représenterOn veut modéliser les systèmest0

interactifs, concourantsa

non déterministes(S, A, −→)
at10

t1

probabilistesbà états possiblement infinist2

ct20

Savoir lescombiner : synchronisation sur étiquettes/actions Acomparer : équivalence, distanceJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Bisimulation [Park et Milner ’80]
Bisimulation : équivalence selon un observateur qui interagit.
(S, A, −→)Exemple typique (fini non probabiliste) :s0s0
a as1bs2zs10


bs20

aa

s100


cs200s1


bs2

a



s10c

s3

acceptent le même langage/les mêmes tracesJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Bisimulation [Park et Milner ’80]
Bisimulation : équivalence selon un observateur qui interagit.
(S, A, −→)Exemple typique (fini non probabiliste) :a as1b



s2zs10bs20t0s0s0aa



s100

s1cb



s200

s2a

s10

t1bc



s3

at2

c



t20

acceptent le même langage/les mêmes tracesJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Bisimulation [Park et Milner ’80]
Bisimulation : équivalence selon un observateur qui interagit.
(S, A, −→)Exemple typique (fini non probabiliste) :a as1b



s2zs10bs20t0s0s0aa



s100

s1cb



s200



s2a



s10

t1bc



s3at2

c



t20

acceptent le même langage/les mêmes traces
ne sont pas interchangeables du point de vue del’interactionJosée Desharnais, Université LavalBisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Modélisation et bisimulation Larsen-Skou ’93
Système de transitions probabiliste (S, A, {Pa }a∈A )sa .3

4a•a .3•?N o∼•

b .1b .4

a .3

b?

bJosée Desharnais, Université LavalBisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Modélisation et bisimulation Larsen-Skou ’93
Système de transitions probabiliste (S, A, {Pa }a∈A )X
Pa : S × S → [0, 1] satisfaisant
Pa (s, t) ≤ 1.
t∈S

sa .3

4a•

a .3

•

?N o∼•b .1b .4

a .3

b?

bJosée Desharnais, Université LavalBisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Modélisation et bisimulation Larsen-Skou ’93
Système de transitions probabiliste (S, A, {Pa }a∈A )X
Pa : S × S → [0, 1] satisfaisant
Pa (s, t) ≤ 1.
t∈SUne bisimulation est une relation d’équivalence qui préserveles probabilités sur les classes d’équivalences.
sa .3

4a•

a .3

•

?N o∼•b .1b .4

a .3b?

bJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Modélisation et bisimulation Larsen-Skou ’93
Système de transitions probabiliste (S, A, {Pa }a∈A )X
Pa : S × S → [0, 1] satisfaisant
Pa (s, t) ≤ 1.
t∈S

Une bisimulation est une relation d’équivalence qui préserveles probabilités sur les classes d’équivalences.
tsa .34a•a .3•b .4?N o

a .3


ba .6

∼•?



4b .1

a .3

•

•

b .5

a?
b |bb?
Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

LICS97 LMP : Labelled Markov Processes
Et si l’ensemble d’états est infini continu ?
alors la probabilité d’un point est nulle !

sPa/Josée Desharnais, Université Laval

X

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

LICS97 LMP : Labelled Markov Processes
Et si l’ensemble d’états est infini continu ?
alors la probabilité d’un point est nulle !
On doit utiliser des mesures

sPa/

Josée Desharnais, Université LavalX

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

LICS97 LMP : Labelled Markov Processes
Et si l’ensemble d’états est infini continu ?
alors la probabilité d’un point est nulle !
On doit utiliser des mesures
Un système de Markov étiqueté (S, Σ, A, {Pa }a∈A )Pa : S × Σ −→ [0, 1] un noyau stochastique,sPa/Josée Desharnais, Université LavalX

Pa (s, S) ≤ 1

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

LICS97 LMP : Labelled Markov Processes
Et si l’ensemble d’états est infini continu ?
alors la probabilité d’un point est nulle !
On doit utiliser des mesures
Un système de Markov étiqueté (S, Σ, A, {Pa }a∈A )(S, Σ) un ensemble d’états (espace analytique)
Pa : S × Σ −→ [0, 1] un noyau stochastique,sPa/Josée Desharnais, Université LavalX

Pa (s, S) ≤ 1

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Bisimulation entre LMP (S, Σ, P)
Definition
Une relation d’équivalence R est une bisimulation sur S sisi s R s0 , et si X est un ensemble R-clos de Σ, alors
Pa (s, X ) = Pa (s0 , X ) pour tout a ∈ Asa .3

4a

•

a .3~

•

b .40?obba .3a .6




∼
•

4b .1



~

ta .3

?

Josée Desharnais, Université Laval

•

~a•

b .5



?nb

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Bisimulation entre LMP (S, Σ, P)
Un ensemble est R-clos si si s ∈ X and sRs0 alors s0 ∈ X .
Definition
Une relation d’équivalence R est une bisimulation sur S sisi s R s0 , et si X est un ensemble R-clos de Σ, alors
Pa (s, X ) = Pa (s0 , X ) pour tout a ∈ A
sa .3

4a

•

a .3~

•b .40?ob



ba .3

a .6




∼
•

4b .1

~

ta .3?

Josée Desharnais, Université Laval•~a•b .5

?nb

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Bisim. finie Bisim. finie probabiliste Bisim. LMP Conclusion

Ici termine le contenu deRichard Blute, Abbas Edalat, Josée Desharnais, Prakash
Panangaden, Bisimulation for Labelled Markov Processes.
LICS 1997.
Prix test-of-time LICS 2017
Définition des LMP
Définition (catégorique) de bisimulation
Démonstration que c’est bien une équivalence
Transitivité de bisimilation difficile !

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Les LMP en main, on veut aussi
se donner un langage pour décrire des propriétésdéterminer si une propriété est satisfaite par unétat/systèmeJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Les LMP en main, on veut aussi
se donner un langage pour décrire des propriétésdéterminer si une propriété est satisfaite par unétat/systèmedémontrer que les propriétés sont complètes pour labisimulation, c.-à-d. :ThéorèmeDeux LMP sont bisimilaires ssi ils satisfont exactement lesmêmes formules.

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Logique : syntaxe et sémantique

L ::== T | φ1 ∧ φ2 | haiq φs |= haiq φssiq ∈ Q ∩ [0, 1]

Pa (s, JφK) ≥ qoù JφK := {s ∈ S | s |= φ}∈ ΣJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002Intro Caractérisation Quoi ? Conclusion

Logique : syntaxe et sémantique
L ::== T | φ1 ∧ φ2 | haiq φs |= haiq φssiq ∈ Q ∩ [0, 1]

Pa (s, JφK) ≥ qoù JφK := {s ∈ S | s |= φ}∈ Σ

s1

a .4
b

•

~

s2~

a .6

s3c!

b

•



•

t1

a .5b

•

~

s1 |= haix hbi1 T pour x ≥ .4|= hai.4 (hbi1 T ∧ hci1 T)

Josée Desharnais, Université Lavalt2,3~

a .5c!

b•Q

bt3&•at1 |= hai.5 hbi1 hai1 hai1 T

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Logique : syntaxe et sémantique

L ::== T | φ1 ∧ φ2 | haiq φs |= haiq φssiq ∈ Q ∩ [0, 1]

Pa (s, JφK) ≥ qoù JφK := {s ∈ S | s |= φ}∈ ΣThéorème (DEP, LICS 1998, I & C 2002)
Deux LMP sont bisimilaires ssi ils satisfont les mêmes formulesde L.

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Quoi ? ? ?
L ::== T | φ1 ∧ φ2 | haiq φq ∈ Q ∩ [0, 1]

Ce résultat a beaucoup surpris. Cette logique :ne contient pas de négation (ni de ou)
ne contient pas de conjonction infinie
Dans le cas non probabiliste ces éléments sont nécessaires

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Quoi ? ? ?
L ::== T | φ1 ∧ φ2 | haiq φq ∈ Q ∩ [0, 1]

Ce résultat a beaucoup surpris. Cette logique :ne contient pas de négation (ni de ou)
ne contient pas de conjonction infinie
Dans le cas non probabiliste ces éléments sont nécessaires
s0as1



t0
a



s2




t1

bs3a



bt2

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Quoi ? ? ?
L ::== T | φ1 ∧ φ2 | haiq φq ∈ Q ∩ [0, 1]

Ce résultat a beaucoup surpris. Cette logique :ne contient pas de négation (ni de ou)
ne contient pas de conjonction infinie
Dans le cas non probabiliste ces éléments sont nécessaires
s0
as1



t0
a



s2




t1

bs3

a



bt2

Josée Desharnais, Université Lavalu0


a



av0R
au1
u2
a..
.

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Caractérisation Quoi ? Conclusion

Le non déterminisme est différent du stochastiqueDans le cas probabiliste, les contre-exemples tombent !
t0s0
a[p]

a[q]

s1s2




t1bs3

a[r ]

bt2

si p + q < r ou p + q > r , alors un haix > les distingue.
si p + q = r et p > 0 alors q < r donc hair hbi1 > lesdistingue.

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Distance Impact

La bisimulation est trop forte !
La bisimulation est utilecomme notion théorique d’égalité (valider autres notions)pour réduire la taille de l’espace des étatsvoir si un processus continu est équivalent à un finiJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Distance Impact

La bisimulation est trop forte !
La bisimulation est utilecomme notion théorique d’égalité (valider autres notions)pour réduire la taille de l’espace des étatsvoir si un processus continu est équivalent à un fini
Mais est trop forte :petite différence de probabilités ⇒ non-bisimilaires
souvent les probabilités sont des valeurs approximatives
spécification finie pour un système infini : comment
valider ?

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Distance Impact

La bisimulation est trop forte !
La bisimulation est utilecomme notion théorique d’égalité (valider autres notions)pour réduire la taille de l’espace des étatsvoir si un processus continu est équivalent à un finiMais est trop forte :petite différence de probabilités ⇒ non-bisimilaires
souvent les probabilités sont des valeurs approximatives
spécification finie pour un système infini : commentvalider ?
Solutions : -bisimulation, simulation (notion de ≤), distanceJosée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Distance Impact

Distance entre les processus – propriétésd(P, Q) = 0 ssi P et Q sont bisimilaires
Convergence en probabilité : On veut ar − .P −−→ ar .P.
→0Et de façon plus générale d(ar −1 .P, ar −2 .P) ≤ |1 − 2 |.
Convergence en profondeur. On veut an .1 −−−→ a∞n→∞Convergence en logiqueNon-expansion par rapport aux opérateurs de l’algèbre deprocessus. Ex. : d(P||R, Q||R) ≤ d(P, Q).
Implémentée à l’aide de la programmation linaire [VanBreugel]Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Intro Distance Impact

Dernier Prix test-of-time LICS 2022
Josée Desharnais, Vineet Gupta, Prakash Panangaden, Radha
Jagadeesan. The Metric Analogue of Weak Bisimulation forProbabilistic Processes. LICS 2002.
This landmark paper is a tour de force, applying new techniques innovel ways to support what constitutes groundbreaking research into
how to analyse probabilistic processes and their applications, invaried domains such as security (including privacy and informationflow), fuzzy systems, control systems, mobile process theory,
software engineering, programming language theory, formal methods,
and coalgebraic process theory, among others.

Josée Desharnais, Université Laval

Bisimulation et distance pour processus probabilistes continus

LICS 1997 Logique LICS 2002

Josée Desharnais, Université Laval

Intro Distance Impact

Bisimulation et distance pour processus probabilistes continus