1 of 25

Minimising the �Probabilistic Bisimilarity Distance

Stefan Kiefer and Qiyi Tang

CONCUR 2024

2 of 25

I. Probabilistic Bisimilarity Distance

3 of 25

Probabilistic Bisimilarity [Larsen & Skou,1991]

s and t are probabilistically bisimilar.

fair coin

fair coin

Labelled Markov chains (LMCs)

Computing probabilistic bisimilarity for LMCs is P-hard. [Chen, van Breugel & Worrell, 2011].

Make tools like PRISM and Storm efficient.

4 of 25

Probabilistic Bisimilarity

s, t1, t2 are not probabilistically bisimilar.

Probabilistic bisimilarity is not robust [Giacalone, Jou & Smolka, 1990].

fair coin

biased coin

biased coin

5 of 25

Probabilistic Bisimilarity Distances �[Desharnais et al., 1999]

The bigger the distance, the more different the two systems behave.

d(s, t1) = 0.49 and d(s, t2) = 0.01

d(s, t) = 0 iff s and t are probabilistically bisimilar.

fair coin

biased coin

biased coin

6 of 25

Probabilistic Bisimilarity Distances

Coupled LMC

7 of 25

Probabilistic Bisimilarity Distances

Coupled LMC

Computing distances for LMCs is polynomial time. [Chen, van Breugel & Worrell, 2011]

8 of 25

II. Motivating Examples for �Minimising Distances

9 of 25

Markov Decision Processes (MDPs)

10 of 25

Markov Decision Processes (MDPs)

MDP + Strategy -> LMC

x%

1 - x%

x%

1 - x%

- deterministic/randomised

- memoryless/general

11 of 25

Minimising Distances for MDPs

The program with two threads, observable value l and secret value h

The secret value h = 0

The secret value is h = 1

scheduler == strategy

12 of 25

Minimising Distances for MDPs

x%

1 - x%

The program with two threads, observable value l and secret value h

x%

1 - x%

Let me see what the secret is…

The secret value h = 0

The secret value is h = 1

13 of 25

Minimising Distances for MDPs

50%

50%

50%

50%

The program with two threads, observable value l and confidential value h

I see no difference

Minimised distance is zero

The secret value h = 0

The secret value is h = 1

14 of 25

Minimising Distances for MDPs

50%

50%

50%

50%

Minimised distance is 1-p

The secret value h = 0

The secret value is h = 1

15 of 25

III. Results

16 of 25

Summary of the Minimisation Problems

  • Link to probabilistic noninterference, a notion in security.
  • Summary of results on distance minimisation problems.

17 of 25

Distance Less Than One

Given two states s, t of an MDP, whether there is a general strategy such that d(s, t) < 1.

It is EXPTIME-complete.

​

For finite LMCs, d(s, t) < 1 iff (s, t) can reach a pair (u, v) with d(u, v) = 0.

For infinite state LMCs, it does not always hold.

​

​

​

​

​

Coupled LMC

18 of 25

Distance Less Than One

We show that there is a general strategy such that d(s, t) < 1 iff there is a general strategy such that in the induced LMC (s, t) can reach a pair (ρ1, ρ2) such that d(ρ1, ρ2) = 0.

Both upper bound and lower bound are based on the general bisimilarity problem, which is known to be EXPTIME-complete [Kiefer & T., 2022].

Upper bound: compute the pairs that can be made bisimilar (in EXPTIME), then determine whether (s, t) can reach any such pair in the coupled graph (polynomial time).

19 of 25

Memoryless Distance Minimisation Problem

  •  

20 of 25

Memoryless Distance Minimisation Problem

x1

1-x1

x2

1-x2

x3

1-x3

x4

1-x4

 

A memoryless strategy

21 of 25

Conclusion

Distance Minimisation Problems

​

​

​

Reduce from the emptiness problem of probabilistic automata.

​

Thank you!

22 of 25

General Distance Minimisation Problem

​

Emptiness problem of probabilistic automata:

23 of 25

Future Work

Distance Maximisation Problems

24 of 25

Probabilistic Bisimilarity Distances

25 of 25

Probabilistic Bisimilarity Distances

Computing distances for LMCs is polynomial time. [Chen, van Breugel, Worrell. 2011]