NC State University, USA

Limiting Behavior of Infinite State Markov Chains

Parosh	Noomene

Abdulla	Ben Henda

Richard	Sven

Mayr	Sandberg

Uppsala University, Sweden

About the Presentation

Paper at QEST '06

Extended version of
conference presentation

See TAPVES homepage
for reference

Overview

Background

Models

Algorithm

Conclusion

Background Models Algorithm Conclusion

Overview

Background

Models

Algorithm

Conclusion

Background Models Algorithm Conclusion

Applications

Program Verification

Communication protocols

Hardware

Probabilistic Models

Unreliable communication

Randomized algorithms

Fault-Tolerant systems

Infinite-State Systems

Unbounded queues, stacks, ...

Time

Unbounded parallelism

Background Models Algorithm Conclusion

Applications

Program Verification

Communication protocols

Hardware

Probabilistic Models

Unreliable communication

Randomized algorithms

Fault-Tolerant systems

Infinite-State Systems

Unbounded queues, stacks, ...

Time

Unbounded parallelism

Background Models Algorithm Conclusion

Limiting Behavior:
Examples

Measures of “long run”-behavior:

How often is a given component used
“in the long run”?

“Average” memory
used by the
operating system

“Average” waiting time
at a traffic light

Background Models Algorithm Conclusion

Limiting Behavior:
Steady State Distribution

Probability distribution over states

πs is the probability to be in s in the long run

Defined on strongly connected systems
(every state is reachable from every state)

Independent of initial state

Background Models Algorithm Conclusion

Limiting Behavior:
Limiting Average Expected Reward

You earn f(s) öre for visiting state s

Then Gsinit(f ) is your expected average income per step, if you start in sinit

Background Models Algorithm Conclusion

Background Models Algorithm Conclusion

s

t

3

6

0.5

0.5

Limiting Behavior:
Steady State πs vs Limiting Average Gsinit(f )

Background Models Algorithm Conclusion

s

t

3

6

0.5

0.5

πs =

2

3

πt =

1

3

Limiting Behavior:
Steady State πs vs Limiting Average Gsinit(f )

Background Models Algorithm Conclusion

s

t

3

6

0.5

0.5

πs =

2

3

πt =

1

3

Gt(f ) = Gs(f ) = 6∙ + 3∙ = 5

2

3

1

3

Limiting Behavior:
Steady State πs vs Limiting Average Gsinit(f )

sinit

Background Models Algorithm Conclusion

s

t

u

7

3

8

6

0.5

0.6

0.4

0.5

πs =

Gt(f ) = Gs(f ) = 6∙ + 3∙ = 5

2

3

1

3

2

3

πt =

1

3

Limiting Behavior:
Steady State πs vs Limiting Average Gsinit(f )

sinit

Background Models Algorithm Conclusion

s

t

u

7

3

8

6

0.5

0.6

0.4

0.5

πs =

πu = 1

Gt(f ) = Gs(f ) = 6∙ + 3∙ = 5

2

3

1

3

2

3

πt =

1

3

Limiting Behavior:
Steady State πs vs Limiting Average Gsinit(f )

sinit

Background Models Algorithm Conclusion

s

t

u

7

3

8

6

0.5

0.6

0.4

0.5

πs =

πu = 1

Gt(f ) = Gs(f ) = 6∙ + 3∙ = 5

2

3

1

3

2

3

πt =

1

3

Gu(f ) = 8∙1= 1

Limiting Behavior:
Steady State πs vs Limiting Average Gsinit(f )

sinit

Background Models Algorithm Conclusion

s

t

u

7

3

8

6

0.5

0.6

0.4

0.5

πs =

πu = 1

Gt(f ) = Gs(f ) = 6∙ + 3∙ = 5

2

3

1

3

2

3

πt =

1

3

Gu(f ) = 8∙1= 1

Gsinit(f ) = 0.4∙5 + 0.6∙1 = 2.6

Limiting Behavior:
Steady State πs vs Limiting Average Gsinit(f )

Overview

Background

Models

Algorithm

Conclusion

Background Models Algorithm Conclusion

Markov Chains

Infinite set of states (countable)

0.5

1

...

...

0.3

0.2

0.5

Background Models Algorithm Conclusion

0.5

Markov Chains

Infinite set of states (countable)
Outgoing transitions sum to 1

0.5

1

...

...

0.2

0.5

Background Models Algorithm Conclusion

0.5

0.3

Finite Eager Attractor

Finite set of states

Background Models Algorithm Conclusion

Finite Eager Attractor

Finite set of states

prob 1

Attractor:

Background Models Algorithm Conclusion

Finite Eager Attractor

Finite set of states

length ≥ n

prob ≤ c·αn

prob 1

Attractor:

Eager:

Background Models Algorithm Conclusion

Finite Eager Attractor

Background Models Algorithm Conclusion

Path Length

1

c·αn

Probability

length ≥ n

prob ≤ c·αn

Eager:

Finite
Eager
Attractor

Example:
Climbing an Infinite Ladder

`

0

Background Models Algorithm Conclusion

Example:
Climbing an Infinite Ladder

`

`

`

`

3

1

...

0

1

2

Background Models Algorithm Conclusion

Example:
Climbing an Infinite Ladder

`

`

`

`

`

3

p

p

p

1-p

1-p

1

1-p

...

0

1

2

Background Models Algorithm Conclusion

Example:
Climbing an Infinite Ladder

`

`

`

`

`

3

p

p

p

1-p

1-p

1

1

1-p

...

0

1

2

Background Models Algorithm Conclusion

Example:
Climbing an Infinite Ladder

`

`

`

`

`

p

p

p

1-p

1-p

1

1

1-p

...

3

0

1

2

Finite Eager Attractor

Background Models Algorithm Conclusion

Example:
Climbing an Infinite Ladder

`

`

`

`

`

p

p

p

1-p

1-p

1

1

1-p

...

Finite Eager Attractor

1

4

1

4

1

4

1

8

1

16

Steady state distribution for p = 0.5

3

0

1

2

Background Models Algorithm Conclusion

Example: Probabilistic Lossy Channel Systems (PLCS)

Finite state processes

Unbounded lossy channels

Send & receive operations

Motivation: Link protocols

Process 1

Process 2

Process 3

Background Models Algorithm Conclusion

Example: Probabilistic Lossy Channel Systems (PLCS)

!m

?n

Sufficient:

One process

One channel

Send & receive operations

m n n m …

A

B

D

C

Infinite state space

Perfect channel = Turing Machine

Background Models Algorithm Conclusion

Example: Probabilistic Lossy Channel Systems (PLCS)

State: s = (A, mnnn)

!m

?n

m n n m …

A

B

D

C

Background Models Algorithm Conclusion

Example: Probabilistic Lossy Channel Systems (PLCS)

Transitions:

!m

?n

m n n m …

A

B

D

C

m n n m … m

!m

Send

A

B

Background Models Algorithm Conclusion

Example: Probabilistic Lossy Channel Systems (PLCS)

Transitions:

m m n n m …

?m

A

B

Receive

!m

?n

m n n m …

A

B

D

C

m n n m … m

!m

Send

A

B

Background Models Algorithm Conclusion

Example: Probabilistic Lossy Channel Systems (PLCS)

Transitions:

m m n n m …

?m

A

B

Receive

!m

?n

m n n m …

A

B

D

C

m n n m … m

!m

Send

A

B

Background Models Algorithm Conclusion

No-op

A

B

Example: Probabilistic Lossy Channel Systems (PLCS)

Background Models Algorithm Conclusion

!m

?n

A

C

D

B

Probabilities are determined by weights

w = 5

w = 3

w = 2

(A, mnnm)

Example: Probabilistic Lossy Channel Systems (PLCS)

Background Models Algorithm Conclusion

!m

?n

A

C

D

B

Probabilities are determined by weights

w = 5

w = 3

w = 2

Not enabled!

(A, mnnm)

Example: Probabilistic Lossy Channel Systems (PLCS)

Background Models Algorithm Conclusion

!m

?n

A

C

D

B

Probabilities are determined by weights

w = 5

w = 3

w = 2

Not enabled!

(A, mnnm)

sum of enabled weights = 5 + 3 = 8

Example: Probabilistic Lossy Channel Systems (PLCS)

Background Models Algorithm Conclusion

!m

?n

A

C

D

B

Probabilities are determined by weights

w = 5

prob =

w = 3

prob =

w = 2

Not enabled!

sum of enabled weights = 5 + 3 = 8

5

8

3

8

(A, mnnm)

Example: Probabilistic Lossy Channel Systems (PLCS)

Probabilistic message loss:

p m n p n …

p n n …

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

Background Models Algorithm Conclusion

Example: Probabilistic Lossy Channel Systems (PLCS)

Finite Eager Attractor:

(A, ε)

The channel will eventually be empty

with prob 1

exponentially fast

(C, ε)

(B, ε)

(D, ε)

Background Models Algorithm Conclusion

Overview

Background

Models

Algorithm

Conclusion

Background Models Algorithm Conclusion

Our Contribution

Approximate steady state distribution

{ πs : s is a state}

for Markov Chains with a finite eager attractor

Assume strongly connected graph

Background Models Algorithm Conclusion

Algorithm: First Idea

Known fact:

(steady state value πs)

= 1 / (expected return time ms)

s

Background Models Algorithm Conclusion

Algorithm: First Idea

Known fact:

(steady state value πs)

= 1 / (expected return time ms)

where

(expected return time ms)

= Σ i · Prob(return to s in i steps)

∞

i =1

Background Models Algorithm Conclusion

Algorithm: First Idea

Known fact:

(steady state value πs)

= 1 / (expected return time ms)

where

(expected return time ms)

= Σ i · Prob(return to s in i steps)

≈ Σ i · Prob(return to s in i steps)

∞

i =1

n

i =1

Background Models Algorithm Conclusion

how big?

Algorithm: First Idea

Known fact:

(steady state value πs)

= 1 / (expected return time ms)

where

(expected return time ms)

= Σ i · Prob(return to s in i steps)

≈ Σ i · Prob(return to s in i steps)

∞

i =1

n

i =1

Background Models Algorithm Conclusion

Nonterminating Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Background Models Algorithm Conclusion

Nonterminating Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Approximation

Step:

i = 1

Background Models Algorithm Conclusion

Nonterminating Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Approximation

Step:

i = 1

i = 2

Background Models Algorithm Conclusion

Nonterminating Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Approximation

Step:

i = 1

i = 2

i = 3

Background Models Algorithm Conclusion

Nonterminating Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Approximation

Step:

i = 1

i = 2

i = 3

i = 4

Background Models Algorithm Conclusion

Nonterminating Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Approximation

Step:

converges

after ∞ steps

i = 1

i = 2

i = 3

i = 4

Background Models Algorithm Conclusion

Nonterminating Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

converges

after ∞ steps

How many steps do we need?

We don't know!

Approximation

Step:

i = 1

i = 2

i = 3

i = 4

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

approximation

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

i = 1

Approximation

Step:

approximation

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

i = 1

i = 2

Approximation

Step:

approximation

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

i = 1

i = 2

i = 3

Approximation

Step:

approximation

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

i = 1

i = 2

i = 3

Approximation

Step:

i = 4

approximation

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

i = 1

i = 2

i = 3

Approximation

Step:

i = 4

i = m

area ≤ 1 + ε

...

approximation

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

i = 1

i = 2

i = 3

Approximation

Step:

i = 4

i = m

area ≤ 1 + ε

...

approximation

error = area ≤ 2·ε

finite

Background Models Algorithm Conclusion

Algorithm

s1 s2 s3 ... states

value of πs

0

1

0.5

correct

values

Q

Q Q

area ≥ 1 – ε

error = area ≤ ε ≈ 0

i = 1

i = 2

i = 3

Approximation

Step:

i = 4

i = m

area ≤ 1 + ε

...

approximation

error = area ≤ 2·ε

finite

Total error ≤ 3·ε

Background Models Algorithm Conclusion

How to Find Q

A

Finite eager attractor

A≤1

A≤2

A≤3

A≤4

...

Q = A≤k = { states reachable in ≤ k steps from A }

k “big”

Background Models Algorithm Conclusion

length ≥ k

prob ≤ c·αk

πs small

How to Find Q

A

Finite eager attractor

A≤1

A≤2

A≤3

A≤4

...

Q = A≤k = { states reachable in ≤ k steps from A }

k “big”

Background Models Algorithm Conclusion

Algorithm – Summary

1. Compute Q

States reachable in k steps from A

Forward path exploration from A

2. Set πs ≈ 0 for s – Q

3. Approximate πs for s – Q

Approximate infinite sum by finite sum

Use forward path exploration from Q

s

A

A≤1

A≤2

A≤3

A≤4

...

Background Models Algorithm Conclusion

Algorithm Approximating
Limiting Average Expected Reward

sinit

Background Models Algorithm Conclusion

Bottom

Strongly

Connected

Components

Algorithm Approximating
Limiting Average Expected Reward

sinit

Background Models Algorithm Conclusion

Bottom

Strongly

Connected

Components

{ πs }

{ πs }

{ πs }

1

2

3

Algorithm Approximating
Limiting Average Expected Reward

sinit

{ πs }

G2(f )

{ πs }

G3(f )

{ πs }

G1(f )

1

2

3

Background Models Algorithm Conclusion

Bottom

Strongly

Connected

Components

Algorithm Approximating
Limiting Average Expected Reward

sinit

p1

p2

p3

Background Models Algorithm Conclusion

Bottom

Strongly

Connected

Components

{ πs }

G2(f )

{ πs }

G3(f )

{ πs }

G1(f )

1

2

3

Algorithm Approximating
Limiting Average Expected Reward

sinit

Gsinit(f ) = p1∙G1(f ) + p2∙G2(f ) + p1∙G1(f )

Bottom

Strongly

Connected

Components

p1

p2

p3

Background Models Algorithm Conclusion

{ πs }

G2(f )

{ πs }

G3(f )

{ πs }

G1(f )

1

2

3

Approximating Gsinit(f ):
Summary

Background Models Algorithm Conclusion

Approximate { πs } in every BSCC

Approximate Gi(f ) in every BSCC (using { πs })

Approximate prob. pi to reach i th BSCC from sinit

Return ∑ Gi(f ) ∙ pi

i

Overview

Background

Models

Algorithm

Conclusion

Background Models Algorithm Conclusion

Conclusions

We consider PLCS, known to have a
finite eager attractor.

Algorithm approximates
steady state distribution.

We generalize it to
limiting average expected reward.

Background Models Algorithm Conclusion

Other models, e.g.,

Petri Nets

Noisy Turing Machines

Compute πs

Approximate πs or
Decide “is πs > x?”

Probabilistic Games

Future Work

Background Models Algorithm Conclusion

The End

Thank you!

Questions?

Background Models Algorithm Conclusion

TAPVES Discussion

Scope

Narrow (research paper) vs. broad (overview)

Program Verification

Time

Thursday Afternoon

Feedback

On presentation technique

On research topic

Background Models Algorithm Conclusion Bonus Slide!

Related work

Different preconditions

Eager attractor

Background Models Algorithm Conclusion Bonus Slide!

Formal Definition:
Steady State Distribution

πs = ∑ πs' ∙ P(s', s)

∑ πs = 1

s is a state

s' is a state

{ πs } is the unique solution to the above system

Background Models Algorithm Conclusion Bonus Slide!

Formal Definition:
Cesàro Limit

Generalizes lim an

Defined even for, e.g., {0, 1, 0, 1, 0, 1, ... }
clim an =

clim an = lim ∙ ∑ ai

n → ∞

n → ∞

1

2

1

n

i =1

n → ∞

n → ∞

n

Background Models Algorithm Conclusion Bonus Slide!

Formal Definition:
Limiting Average Expected Reward

clim “Expected reward in nth step”

n → ∞

Background Models Algorithm Conclusion Bonus Slide!

L.A.E.R. =

Formal Definition:
Limiting Average Expected Reward

clim “Expected reward in nth step”

= clim ∑ Prob(ρ) ∙ f(ρ)

where

f(s1s2∙∙∙sn) = f(s1) + f(s2) + ... + f(sn)

n → ∞

ρ is a path

starting in sinit

of length n

n → ∞

Background Models Algorithm Conclusion Bonus Slide!

L.A.E.R. =

2006-09-05T17:55:13