Steady-state probabilities

Loading...

From the course by EIT Digital

Quantitative Model Checking

26 ratings

EIT Digital

Quantitative Model Checking

26 ratings

The integration of ICT (information and communications technology) in different applications is rapidly increasing in e.g. Embedded and Cyber physical systems, Communication protocols and Transportation systems. Hence, their reliability and dependability increasingly depends on software. Defects can be fatal and extremely costly (with regards to mass-production of products and safety-critical systems). First, a model of the real system has to be built. In the simplest case, the model reflects all possible states that the system can reach and all possible transitions between states in a (labelled) State Transition System. When adding probabilities and discrete time to the model, we are dealing with so-called Discrete-time Markov chains which in turn can be extended with continuous timing to Continuous-time Markov chains. Both formalisms have been used widely for modeling and performance and dependability evaluation of computer and communication systems in a wide variety of domains. These formalisms are well understood, mathematically attractive while at the same time flexible enough to model complex systems. Model checking focuses on the qualitative evaluation of the model. As formal verification method, model checking analyzes the functionality of the system model. A property that needs to be analyzed has to be specified in a logic with consistent syntax and semantics. For every state of the model, it is then checked whether the property is valid or not. The main focus of this course is on quantitative model checking for Markov chains, for which we will discuss efficient computational algorithms. The learning objectives of this course are as follows: - Express dependability properties for different kinds of transition systems . - Compute the evolution over time for Markov chains. - Check whether single states satisfy a certain formula and compute the satisfaction set for properties.

From the lesson

Discrete Time Markov Chains

We enhance transition systems by discrete time and add probabilities to transitions to model probabilistic choices. We discuss important properties of DTMCs, such as the memoryless property and time-homogeneity. State classification can be used to determine the existence of the limiting and / or stationary distribution.

Steady-state probabilities12:09

Meet the Instructors

Anne Remke
Prof. dr.
Computer Science

[MUSIC]

So, before we are computing the steady state probabilities

in this last last lecture of that module, we first have to take

a look at two more concepts, mainly Irreducibility and periodicity.

What does irreducibility mean?

Well, a is irreducible if

from each state we can reach each other state in a finite number of steps.

That one is easy.

Now what is the period d(s) of state s.

If we want to compute the period for a state, we first need to find the greatest

common divisor for all values step numbers n for

which we have a positive probability to coming back to that state.

Then if this greatest common divisor is greater than one,

the state s is called periodic.

And if this greatest common divisor equals one,

the state is called aperiodic.

Now if you want to formalize this, we have this equation,

and it states, then it states S is periodic

if exist such as greatest common division d.

Which is greater than one, such that fo all N and

mod d Is not equal to zero, it follows that PSSN is zero.

So there's a zero probability to returning to that state as in

N time steps.

In a DTMC, that is good to know that all

states in the same component have the same period.

So what does a component?

A component is a part of the DTMC that is irreducible basically.

All states in that component are reachable from each other.

And that also means if the complete DTMC is irreducible, all states

in that DTMC are either periodic with the same period or they are all aperiodic.

Now, let's take a look at a simple example.

We have DTMC with four states and

we want to check whether it is irreducible or not.

Well, this DTMC clearly is irreducible,

because you can reach each state from each other state.

Now, what about the periodicity?

For that We have to pick one state, I picked state 0.

And we have to check with how many steps you can

come back to that state, so you can come back in.

In one, two, three steps or in one, two, three, four, five, six steps.

So three, six, nine, and you immediately see

that the greatest common divisor of all these step numbers is three.

So we can state that this DTMC

is periodic with

DS3 we have stated that it is irreducible

and now I want to take the opportunity and also.

See whether you can remember the concepts from last lecture, so

are these states transient or recurrent?

What do you think?

Well they're recurrent because they are all in the same component,

and there is a zero probability to leave this component.

What you see is also that in a finite DTMC the concept of irreducability and

recurrence, actually talks about similar things.

Only in infinite DTMCs you really

have to distinguish the two.

Now, what about the long run behavior of this DTMC?

We need a starting state which is state 0, in this case.

Now let me write down the first transient distributions for,

time point zero, this is one, zero, zero, zero.

For the next time point, one, this is zero,

one third, two third, zero.

One more, we have zero, zero 0, 1,

and then in the next one,

we have 1, 0, 0, 0, which you've seen before.

So what you see is that the limiting behavior here doesn't exist, but

What you do see if you take a look at the first six distributions is a pattern.

Namely, for all step numbers that are multiples of i,

you have the same vector, 1,0,0,0 for

all step numbers that are multiples of 3 plus 1 you have 0,

one-third, two-third zero.

And for all step numbers that are multiples of 3 + 2 you have 0, 0, 0, 1.

And this clearly is because the is periodic with period three.

Now, let me play around with this DGMC a bit and I want to add a self-loop.

And that is this transition which leaves state 3 and

goes back to state 3 with probability one-half.

Now, if you take a look at this, and

you want to compute the period of that DTMC,

you see that for the first two step numbers, one and two,.

You have a probability zero of returning but for all step numbers that

are at least three, you have a positive probability of returning.

Why is that?

Well that is because you can idle in that self loop as long as you want.

So for example we do one, two, three, four or we do one,

two, three, four, five and the same for all larger step numbers.

Clearly, the greatest common divisor of these step numbers,

is one, which turns this DTMC into an aperiodic DTMC,

for which we can derive the limiting distribution.

I've already hinted at this concept of components and

that mutually reachable states that are in one component have the same type.

This not only holds for reachability, but it also holds for.

Transient, recurrent, positive and

nonrecurrent as well as periodicity.

So, if you have identified a component of mutually reachable state,

it is enough to only consider the characteristics of one of these states.

Now finally, we can move towards a Stationary distribution.

We define the P vector, as the stationary

distribution of DTMC with matrix P,

such that Pi equals pi times p.

That is a matrix vector notation.

You can also write this down per state.

And then we have pi s is the stationary probability for state s.

Equals the sum of the complete state space of pi s

prime times the probability to move from s prime to s.

We can also say this in yet another way, and that is that the probability flow

Out of a certain state has to equal the probability flow into that state.

So, this is for ps, ps times one minus pss.

That's the probability to leave that state.

Equals sum over All states from the state space,

P(s prime) times P(s prime, s), the probability to move from s prime to s.

So there are different ways to express the same thing.

And now we come to the main theorem of this Lecture in and

irreducible, aperiodic and positive recurrent DTMC,

the limiting distribution v exist.

Also, this limiting distribution has been

independent of the initial probability distribution.

So you do not need to consider this.

And, v is equal to the unique stationary, or steady-state, probability distribution.

Now you've seen in this lecture that we've talked about the limiting distribution,

which only exists if the DTMC is a periodic and

we have the stationary or steady-state distribution.

Which may also exist if the DTMC

is aperiodic but I'll tell you how this works on this slide.

So if we have a DTMC that is irreducible and positive recurrent but

not necessarily a periodic, we still have a unique stationary distribution and

that is defined as Pi s equals 1 divided by ms.

Now what is ms, you've seen that before.

And it is the mean number of steps between two successive visits to that state s.

So this is nice because it gives you a way to reason about the long run,

the average behavior even though the DTMC might

be Periodic and with that the limiting distribution does not exist.

So this wraps up my lecture on

the study site distributions and on DTMCs in general and I hope to see you back.

For the next module where we start to do model checking for DTMCs.

[SOUND]

Explore our Catalog

Join for free and get personalized recommendations, updates and offers.

Coursera provides universal access to the world’s best education, partnering with top universities and organizations to offer courses online.

© 2019 Coursera Inc. All rights reserved.

Download on the App Store

Get it on Google Play