Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 34

programming problem:

Maximise s ∈ S ( ʔ ( s ) − ʘ ( s )) x s

(3.7)

subject to •∀ s , t ∈ S : x s − x t ≤ m ( s , t )

•∀ s ∈ S :0 ≤ x s ≤ 1 .

This problem can be dualised and then simplified to yield the following problem:

Minimise s , t ∈ S m ( s , t ) y st
subject to

S : t ∈ S y st =

•∀ s ∈ ʔ ( s )

(3.8)

S : s ∈ S y st = •∀ ∈

t ʘ ( t )

•∀ s , t ∈ S : y st ≥ 0 .

Now ( 3.8 ) is in exactly the same form as ( 3.6 ).
This way of lifting pseudometrics via the Kantorovich metric as given in ( 3.8 ) has
an interesting connection with the lifting of binary relations given in Definition 3.2 .

Theorem 3.3 Let R be a binary relation and m a pseudometric on a state space S

satisfying

s R t iff m ( s , t ) = 0 (3.9)

∈

for any s , t S. Then it holds that

† ʘ

ʔ R iff m ( ʔ , ʘ ) ˆ = 0

for any distributions ʔ , ʘ ∈ D ( S ) .

† ʘ . From Theorem 3.1 (1) we know there is a weight function

Proof Suppose ʔ R

w such that

S : t ∈ S w ( s , t ) 1. ∀ s ∈ = ʔ ( s ).

S : s ∈ S w ( s , t ) 2. ∀ t ∈ = ʘ ( t ).

3. ∀ s , t ∈ S : w ( s , t ) > 0 ⃒ s R t .

By substituting w ( s , t ) for y s , t in ( 3.8 ), the three constraints there can be satisfied.
For any s , t ∈ S we distinguish two cases:

1. Either w ( s , t ) 0;

2. or w ( s , t ) > 0. In this case we have s

=

R t , which implies m ( s , t ) = 0by( 3.9 ).

Therefore, we always have m ( s , t ) w ( s , t ) = 0 for any s , t ∈ S . Consequently, we get

s , t ∈ S m ( s , t ) w ( s , t )

= 0 and the optimal value of the problem in ( 3.8 ) must be 0,

i.e. 0, and the optimal solution is determined by w .

The above reasoning can be reversed to show that the optimal solution of ( 3.8 )
determines a weight function, thus

m ( ʔ , ʘ ) ˆ =

† ʘ .

m ( ʔ , ʘ ) ˆ = 0 implies ʔ R