The Good, the Bad, and the Random
Stochastic Games with Lossy Channels

NC State University, USA

Parosh	Noomene

Abdulla	Ben Henda

Richard	Sven

Mayr	Sandberg

Uppsala University

Overview

Background

Model

Algorithm

Conclusion

Background Model Algorithm Conclusion

Overview

Background

Model

Algorithm

Conclusion

Background Model Algorithm Conclusion

Context

Reactive System

Never terminates

Input & output during execution

Program Verification

Communication protocols

Hardware

One approach to verification:

Model checking

Input: model + formula

Output: “yes, formula true” / “no, formula false”

Background Model Algorithm Conclusion

Context

Reactive System

Never terminates

Input & output during execution

Program Verification

Communication protocols

Hardware

One approach to verification:

Model checking

Input: model + formula

Output: “yes, formula true” / “no, formula false”

Background Model Algorithm Conclusion

Stochastic Infinite-State Games

Stochastic

Unreliable communication

Fault-Tolerant systems

Randomized algorithms

Infinite-State

Unbounded queues, stacks, counters, ...

Time

Unbounded parallelism

Games

Model interacts with environment

Alternation in logics

Abstraction

Background Model Algorithm Conclusion

Stochastic Infinite-State Games

Stochastic

Unreliable communication

Fault-Tolerant systems

Randomized algorithms

Infinite-State

Unbounded queues, stacks, counters, ...

Time

Unbounded parallelism

Games

Model interacts with environment

Alternation in logics

Abstraction

Background Model Algorithm Conclusion

Reachability

F – set of “target states”

F reached?

Example:

Background Model Algorithm Conclusion

F

F

...

Reached

Not reached

F

Repeated Reachability

F – set of “target states”

F reached infinitely often?

Example:

Will it always return to the green state?

Background Model Algorithm Conclusion

F

...

F

...

Infinitely
often

Finitely
often

F

Overview

Background

Model

Algorithm

Conclusion

Background Model Algorithm Conclusion

Lossy Channel Systems (LCS)

Process 1

Process 2

Process 3

Background Model Algorithm Conclusion

Model:

Finite state processes

Unbounded lossy channels

Send & receive operations

Motivation:

Models of communication protocols

Game Probabilistic
Lossy Channel Systems (GPLCS)

Process 1

Process 3

Background Model Algorithm Conclusion

λ

Evil
Cracker

Game:
Interaction with evil cracker

Probabilistic:
Messages lost randomly
(probability λ)

λ

λ

λ

λ

λ

λ

λ

!m

?n

m p p m …

A

D

Game Probabilistic
Lossy Channel Systems (GPLCS)

B

C

Sufficient:

One channel

One process

Each state controlled by a player

Properties:

Infinite state space

Perfect channel = Turing machine

Background Model Algorithm Conclusion

!m

?n

m p p m …

A

D

B

C

State: s = (A, mpnn)

Game Probabilistic
Lossy Channel Systems (GPLCS)

Background Model Algorithm Conclusion

Transitions:

m p p m … m

!m

Send

A

B

!m

?n

m p p m …

A

D

B

C

Game Probabilistic
Lossy Channel Systems (GPLCS)

Background Model Algorithm Conclusion

Transitions:

m m p p m …

?m

A

B

Receive

m p p m … m

!m

Send

A

B

!m

?n

m p p m …

A

D

B

C

Game Probabilistic
Lossy Channel Systems (GPLCS)

Background Model Algorithm Conclusion

Transitions:

m m p p m …

?m

A

B

Receive

m p p m … m

!m

Send

A

B

No-op

A

B

!m

?n

m p p m …

A

D

B

C

Game Probabilistic
Lossy Channel Systems (GPLCS)

Background Model Algorithm Conclusion

Probabilistic message loss:

p m n p n …

p n n …

Each transition:
each message lost with prob λ > 0,
independently

Game Probabilistic
Lossy Channel Systems (GPLCS)

Background Model Algorithm Conclusion

Stochastic Games

Every GPLCS induces a stochastic game

3 types of states:

Player GOOD

Player BAD

Player RANDOM

Background Model Algorithm Conclusion

0.1

0.2

0.7

0.4

0.6

Stochastic Games

Every GPLCS induces a stochastic game

3 types of states:

Background Model Algorithm Conclusion

0.1

0.2

0.7

0.4

0.6

Stochastic Games

Strategy
= selection of outgoing transitions

Strategies for GOOD & BAD
Only probabilistic
choices remain
“Prob(event)”
well-defined

Background Model Algorithm Conclusion

0.1

0.2

0.7

0.4

0.6

Stochastic Games

Strategy
= selection of outgoing transitions

Strategies for GOOD & BAD
Only probabilistic
choices remain
“Prob(event)”
well-defined

Background Model Algorithm Conclusion

0.1

0.2

0.7

0.4

0.6

Background

Models

Algorithm

Conclusion

Overview

Background Model Algorithm Conclusion

Repeated Reachability
for GPLCS

Input:

GPLCS

Set F of final states

Output: Partition of states:

Background Model Algorithm Conclusion

Winning for BAD

Winning for GOOD

GOOD forces

Prob(reach F inf. often) = 1

BAD forces

Prob(reach F inf. often) < 1

Subroutine: Force-set

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Q

Prob > 0

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Q0 = Q

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Q0 = Q

Q1 = 1 step before Q0

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

Q

GOOD states that
can go to Q0

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Q0 = Q

Q1 = 1 step before Q0

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

Q

GOOD states that
can go to Q0

BAD states that
must go to Q0

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Q0 = Q

Q1 = 1 step before Q0

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

Q

GOOD states that
can go to Q0

BAD states that
must go to Q0

RANDOM states that
can go to Q0

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Q0 = Q

Q1 = 1 step before Q0

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

GOOD states that
can go to Q1

BAD states that
must go to Q1

RANDOM states that
can go to Q1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

Background Model Algorithm Conclusion

Subroutine: Force-set
Construction

∙ ∙ ∙

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Qn = 1 step before Qn-1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

Background Model Algorithm Conclusion

Subroutine: Force-set
Convergence

∙ ∙ ∙

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Background Model Algorithm Conclusion

Qn = 1 step before Qn-1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

Converges?

Subroutine: Force-set
Convergence

∙ ∙ ∙

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Background Model Algorithm Conclusion

Qn = 1 step before Qn-1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

Converges?

YES! for GPLCS
(well quasi orders)

Subroutine: Force-set
Correctness

∙ ∙ ∙

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Background Model Algorithm Conclusion

Correct?

Qn = 1 step before Qn-1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

Subroutine: Force-set
Correctness

∙ ∙ ∙

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Background Model Algorithm Conclusion

Correct?

Qn = 1 step before Qn-1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

YES!
(and I'll show why)

Subroutine: Force-set
Correctness

∙ ∙ ∙

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Background Model Algorithm Conclusion

Correct?

Qn = 1 step before Qn-1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

In Qn, GOOD can force
Prob(reach Q ) > 0
by construction

Subroutine: Force-set
Correctness

∙ ∙ ∙

Q

Force-set ≈ “Reachability for games”

Given target set Q

Compute the set of states where
GOOD can force Prob(reach Q) > 0

Backward search

Background Model Algorithm Conclusion

Correct?

Qn = 1 step before Qn-1

Q2 = 1 step before Q1

Q0 = Q

Q1 = 1 step before Q0

In Qn, GOOD can force
Prob(reach Q ) > 0
by construction

Outside Qn, BAD can force
Prob(reach Q ) = 0

island 0

LAND – always food!

. . .

island 1

island 2

island 3

GOOD trapped

BAD trapped

water 0

water 1

water 2

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Background Model Algorithm Conclusion

Algorithm
Idea

Algorithm
Idea

island 0

island 0

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Idea

island 0

island 0

LAND – always food!

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Idea

island 0

island 0

LAND – always food!

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Idea

island 0

island 0

LAND – always food!

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Idea

island 0

island 0

LAND – always food!

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Idea

island 0

island 0

LAND – always food!

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Idea

island 0

island 0

LAND – always food!

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Idea

island 0

island 0

LAND – always food!

LAND – always food!

. . .

island 1

island 2

island 3

BAD trapped

water 0

water 1

water 2

Background Model Algorithm Conclusion

GOOD trapped

A world of islands and water

No food (= F ) on islands

In water, may float to island (possibly elsewhere, too)

Find BAD islands and water!

Algorithm
Overview

Background Model Algorithm Conclusion

F

Algorithm
Overview

Background Model Algorithm Conclusion

Island 0

F

Prob > 0

Compute Q: GOOD can force Prob(reach F) > 0

Q

Algorithm
Overview

Background Model Algorithm Conclusion

Island 0

F

I0

Compute Q: GOOD can force Prob(reach F) > 0

I0 = complement(Q)

So BAD can force Prob(reach F) = 0 on I0

Algorithm
Overview

Background Model Algorithm Conclusion

F

I0

Water 0

Compute Q: BAD can force Prob(reach I0) > 0

Prob > 0

Q

Algorithm
Overview

Background Model Algorithm Conclusion

F

W0

I0

Water 0

Compute Q: BAD can force Prob(reach I0) > 0

W0 = Q

Algorithm
Overview

Background Model Algorithm Conclusion

F

W0

I0

Island 1

Prob > 0

Compute Q:
GOOD can force Prob(reach F) > 0, avoiding I0 and W0

Q

Algorithm
Overview

Background Model Algorithm Conclusion

F

I1

W0

I0

Island 1

Compute Q:
GOOD can force Prob(reach F) > 0, avoiding I0 and W0

I1 = complement(Q)

Algorithm
Overview

Background Model Algorithm Conclusion

F

I1

W0

I0

Prob > 0

Compute Q: BAD can force Prob(reach I0 υ W0 υ I1) > 0

Water 1

Algorithm
Overview

Background Model Algorithm Conclusion

F

W1

I1

W0

I0

Compute Q: BAD can force Prob(reach I0 υ W0 υ I1) > 0

W1 = Q

Water 1

Algorithm
Overview

Background Model Algorithm Conclusion

F

W1

I1

W0

I0

Island 2

Compute Q:
GOOD can force Prob(reach F) > 0, avoiding I0,W0,I1,W1

Q

Prob > 0

Algorithm
Overview

Background Model Algorithm Conclusion

F

I2

W1

I1

W0

I0

Island 2

Compute Q:
GOOD can force Prob(reach F) > 0, avoiding I0,W0,I1,W1

I2 = complement(Q)

Algorithm
Overview

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Algorithm
Convergence

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Converges?

Algorithm
Convergence

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

YES! for GPLCS
(well quasi orders, difficult)

Converges?

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

YES!
(and I'll show why)

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

GOOD can force

Prob(reach F inf. often) = 1

BAD can force

Prob(reach F inf. often) < 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

BAD can force

Prob(reach F inf. often) < 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

In I0:

Prob(reach F inf. often) < 1
(since even

Prob(reach F) = 0)

BAD can force

Prob(reach F inf. often) < 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

In Wn:

Prob(reach F inf. often) < 1
(since Prob(reach In) > 0)

In I0:

Prob(reach F inf. often) < 1
(since even

Prob(reach F) = 0)

BAD can force

Prob(reach F inf. often) < 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

In In:

GOOD chooses how to die:

stay in In and lose (no F )

or go to Wn-1 and lose

In Wn:

Prob(reach F inf. often) < 1
(since Prob(reach In) > 0)

In I0:

Prob(reach F inf. often) < 1
(since even

Prob(reach F) = 0)

BAD can force

Prob(reach F inf. often) < 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

In In:

GOOD chooses how to die:

stay in In and lose (no F )

or go to Wn-1 and lose

In Wn:

Prob(reach F inf. often) < 1
(since Prob(reach In) > 0)

In I0:

Prob(reach F inf. often) < 1
(since even

Prob(reach F) = 0)

So BAD wins

with prob. > 0

in all Wn, In

BAD can force

Prob(reach F inf. often) < 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

GOOD can force

Prob(reach F inf. often) = 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

Convergence means:

No more watern

No more island

GOOD can force

Prob(reach F inf. often) = 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

Convergence means:

No more water	GOOD can stay outside In, Wn

No more island

GOOD can force

Prob(reach F inf. often) = 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

Convergence means:

No more water	GOOD can stay outside In, Wn

No more island	GOOD can force Prob(reach F ) > 0

GOOD can force

Prob(reach F inf. often) = 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

Convergence means:

No more water	GOOD can stay outside In, Wn

No more island	GOOD can force Prob(reach F ) > 0

So GOOD can force:

Always Prob(reach F ) > 0

GOOD can force

Prob(reach F inf. often) = 1

Algorithm
Correctness

Background Model Algorithm Conclusion

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Correct?

So GOOD can force:

Always Prob(reach F ) > 0

Convergence means:

No more water	GOOD can stay outside In, Wn

No more island	GOOD can force Prob(reach F ) > 0

For GPLCS, this implies

Prob(reach F inf. often) = 1

(using attractors, difficult)

GOOD can force

Prob(reach F inf. often) = 1

Background

Models

Algorithm

Conclusion

Overview

Background Model Algorithm Conclusion

The Problem We Studied

GPLCS:
Protocol vs. Cracker

Repeated reachability:
reach “good” state infinitely many times

Process 1

Process 3

λ

Evil
Cracker

λ

λ

λ

λ

λ

λ

λ

F

Background Model Algorithm Conclusion

Algorithm

Force-set:

Prob(reach Q ) > 0

Backward search

Winning sets for BAD:

Prob(reach F inf. often) < 1

Search for islands and water

∙ ∙ ∙

Q

F

∙ ∙ ∙

I2

W1

I1

W0

I0

Background Model Algorithm Conclusion

Extensions

Construct winning strategies

Concurrent games

Simultaneous moves

Reachability games

Can GOOD force Prob(reach F ) = 1 ?

Parity games

Generalization of repeated reachability

Background Model Algorithm Conclusion

Can do

Unclear

The End

Questions?

Background Model Algorithm Conclusion

Convergence:
Well Quasi Orders

Recall:

Subword ordering:
pmp mpmmp

Upward closure:
all “bigger” states

Message loss
subword

State: s = (A, mppp)

(A, mppmm)

(A, mpp)

(A, mmpp)

(A, mp)

∙∙∙

Background Model Algorithm Conclusion Bonus Slide!

Convergence:
Well Quasi Orders

If we can lose some messages...

Background Model Algorithm Conclusion Bonus Slide!

Convergence:
Well Quasi Orders

...then we can lose more!

If we can lose some messages...

Background Model Algorithm Conclusion Bonus Slide!

Convergence:
Well Quasi Orders

...then we can lose more!

If we can lose some messages...

Conclusion:

RANDOM states one step before
are upward closed

Background Model Algorithm Conclusion Bonus Slide!

Convergence of Force-sets:
Well Quasi Orders

Theorem (Higman 1952):
Any sequence of increasing, upward closed sets converges.

We apply it:

∙ ∙ ∙

Q

Player
states

Random
states

Background Model Algorithm Conclusion Bonus Slide!

Convergence of Force-sets:
Well Quasi Orders

Theorem (Higman 1952):
Any sequence of increasing, upward closed sets converges.

We apply it:

∙ ∙ ∙

Q

Player
states

Random
states

Upward closed

terminates!

Background Model Algorithm Conclusion Bonus Slide!

Convergence of Force-sets:
Well Quasi Orders

Theorem (Higman 1952):
Any sequence of increasing, upward closed sets converges.

We apply it:

∙ ∙ ∙

Q

Player
states

Random
states

Upward closed

terminates!

Every 2nd step is a loss

terminates!

Background Model Algorithm Conclusion Bonus Slide!

Convergence of Algorithm:
Well Quasi Orders

Argument is much more difficult!

RANDOM states in water upward closed

Sequence of waters terminates

Sequence of islands terminates

F

I2

W1

I1

W0

I0

Player
states

Random
states

Background Model Algorithm Conclusion Bonus Slide!

The Fine Print:
Finite-Memory Strategies

We assume BAD is restricted to
finite-memory strategies

BAD cannot remember unbounded amount of history

Intuition: Evil cracker has a finite hard disk

Needed to prove correctness

Background Model Algorithm Conclusion Bonus Slide!

Leftover

Process 1

Process 3

λ

Evil
Cracker

λ

λ

λ

λ

λ

λ

λ

Repeated Reachability

F – set of “target states”

Is F reached infinitely often?

Example:

Will it always return to the green state?

Background Model Algorithm Conclusion

F

2007-03-01T16:19:50