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

to each edge ( v , w ) ∈ E a nonnegative number c ( v , w ). A flow function f for N is a

function that assigns to edge e a real number f ( e ) such that

•0 ≤ f ( e ) ≤ c ( e ) for all edges e .

• Let in ( v ) be the set of incoming edges to node v and out ( v ) the set of outgoing

edges from node v . Then, for each node v

∈ N \{ s ↥ , s } ,

f ( e ) = f ( e ) .

e ∈ in ( v ) e ∈ out ( v )

The flow F ( f )of f is given by

F ( f ) = f ( e ) − f ( e ) .

e ∈ out ( s ↥ ) e ∈ in ( s ↥ )

The maximum flow in N is the supremum (maximum) over the flows F ( f ), where

f is a flow function in .

We will see that the question whether ʔ

N

† ʘ holds can be reduced to a maximum
flow problem in a suitably chosen network. Suppose

R

R ↆ × ∈ D

S S and ʔ , ʘ ( S ).

Let S ={ s |

∈ }

where s are pairwise distinct new states, i.e. (_) : S

ₒ

S

s S

S with

is a bijective function. We create two states s ↥ and s not contained in S ∪

s ↥ = s . We associate with the pair ( ʔ , ʘ ) the following network N ( ʔ , ʘ , R ).

The nodes are N = S ∪ S ∪{ s ↥ , s }

• .

( s , t ) ( s , s )

• The edges are E ={ | ( s , t ) ∈ R }∪{ ( s ↥ , s ) | s ∈ S }∪{ | s ∈ S } .

ʔ ( s ), c ( t , s ) ʘ ( t ) and c ( s , t )

• The capability c is defined by c ( s ↥ , s ) = = = 1

for all s , t ∈ S .

The network is depicted in Fig. 3.3 .
The next lemma appeared as Lemma 5.1 in [ 26 ].

Lemma 3.2 Let S be a finite set, ʔ , ʘ ∈ D ( S ) and R ↆ S × S. The following

statements are equivalent.

(i) There exists a weight function w for ( ʔ , ʘ ) with respect to R .

(ii) The maximum flow in N ( ʔ , ʘ , R ) is 1 .

Proof (i) ⃒ (ii): Let w be a weight function for ( ʔ , ʘ ) with respect to R .We

ʔ ( s ), f ( t , s )

define a flow function f as follows: f ( s ↥ , s ) = = ʘ ( t ) and moreover

= s ∈ S f ( s ↥ , s ) = s ∈ S ʔ ( s ) f ( s , t )

1.
For each outgoing edge ( s ↥ , s ) from node s ↥ , its maximum capacity is reached, so
the maximum flow of

= w ( s , t ) for all s , t ∈ S . Then F ( f ) =

N ( ʔ , ʘ , R )is1.

⃒ =

(ii) (i): Let f be a flow function such that F ( f ) 1. We observe that

≤ =

f ( s ↥ , s ) c ( s ↥ , s ) ʔ ( s ) and

f ( s ↥ , s ) = F ( f ) = 1 = ʔ ( s ),

s ∈ S s ∈ S

so it must be the case that f ( s ↥ , s ) = ʔ ( s ) for all s ∈ S . Similarly, we have the

dual f ( t , s )

= ʘ ( t ) for all t ∈ S . Let w be the weight function defined by letting