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.
Time-bounded Until
Loading...
From the course by EIT Digital
Quantitative Model Checking
23 оценки
From the lesson
Probabilistic Computational Tree Logic
We discuss the syntax and semantics of Probabilistic Computational Tree logic and check out the model checking algorithms that are necessary to decide the validity of different kinds of PCTL formulas. We shortly discuss the complexity of PCTL model checking.
Meet the Instructors
Anne RemkeProf. dr.
Computer Science
[MUSIC]
So let's do the other probability operator now.
The so called Time-bounded Until.
Before we do that I would like to recall the semantics of this Time-bounded Until
operator with you.
So what does it mean?
We want to check for a L-DTMC If this property
phi until psi with a time on k holds or not.
Well this path property small phi is fulfilled once a psi state is
reached in at most case steps a longer path that consists of only psi states.
On the other hand Phi is violated once a state is hit that is neither phi nor psi.
And of course once we have reached the step limit k,
we also violated the formula, if we hadn't reached a psi state.
Let us formalize this.
The probability that a state s fulfills such a formula
is split up into three cases.
The first case, we start in a state s that is a psi state.
Well, if we start there, the formula is immediately valid and
the probability is 1.
On the other hand, if we deal with the state s, that is a phi state, and
not a psi state, then we have a recursive computation.
I'm going to show you, so
here we have such a state s that is phi and not psi.
And what we do is we accumulate the probability for
all states s prime in the state space, and
we multiply the probability to move from s to s prime
with the probability to validate the formula phi onto psi,
but now with one step less, so for k, -1.
This is the second case and then in the third case,
we are not in such a state and the probability is 0.
So for any other state the probability is 0.
Now if we want to apply this, we can solve this
with a fixed-point iteration, but this is very cumbersome.
So instead I'm going to show you a better way to solve this.
And this is what we call the pCTL trick which reduces model
checking the bounded until operator to a transient analysis.
How does this work?
Well, first we have to transform the DTMC that we are checking.
And we make absorbing all psi states,
because once we hit up the psi state we done in the formula holds.
And we have to make absorbing all states that are not phi nor psi,
because if we stumble upon one of these states the formula doesn't hold anymore.
So we make these states absorbing, and then we check for
reachability of psi in the transformed DTMC.
And this reduces to transit analysis, and
we have to accumulate the transient probability to be in
a state that belongs to the satisfaction set of psi at time k.
Then we compare this accumulated probability with the probability bound p.
Either holds, then the formula is valid, or it doesn't hold and
the formula is false.
So let's take a look at an example.
This is the property I would like to check.
Up 3 or up 2 until down in utmost three steps.
You've seen this already in one of the previous lectures.
Now I'm going to replace up 3 up 2 by colors to better visualize the formula.
So this is the DTMC we'll use.
You see we have one red state corresponds to down and
then we have green and blue corresponding to up 3 and up 2.
And we have a white and a yellow state.
Now, I have to make this DTMC absorbing
in the sense that all the red states become absorbing and
all states that are neither green or the blue or red are made absorbing.
What does it mean to make them absorbing?
It simply means we have to remove all the outgoing transitions.
So let me do this for you.
I have to get rid of this one.
And I have to get rid of these two because white is neither green,
blue or red.
And also here in yellow I have to remove all the outgoing transitions.
Now let's see whether I did this correctly.
Yes, looks like it.
So this is the transform DTMC which we use for the transient analysis.
Now for the transient analysis, we need the probabilities on the edges
and from that we derive the P matrix which you need
to compute the trans-improbability distribution after three steps.
Now the only problem is, now that I want to know for each state of this DTMC
whether it fulfills that formula, because I need that for the satisfaction set.
Now, I have to do the transient probability distribution.
For four initial vectors and each time
it represents another state as the only initial state.
So this is how it looks and
now I have to multiply these four vectors to P to the power of 3.
And then, I obtained the transient probability distribution for
each state as a possible starting state.
Now this is fine but it is very cumbersome, so
I would like to note that the so-called forwards computation
requires a single transient analysis for each possible starting state.
Now, if you want to know how to do this more efficiently,
I would recommend to watch the next lecture.
[SOUND]
Ознакомьтесь с нашим каталогом
Присоединяйтесь бесплатно и получайте персонализированные рекомендации, обновления и предложения.
Coursera делает лучшее в мире образование доступным каждому, предлагая онлайн-курсы от ведущих университетов и организаций.
© Coursera Inc., 2018 Все права защищены.
