Welcome everybody to another tutorial of Formula in Methods.

Today we are going to do something more theoretical than usual in the tutorials as well, because

there's not enough time in the lecture to cover all the model checking algorithms.

You've learned how to model check against CTL formulas in the lecture and today I'm

going to tell you how we can do LTL model checking.

So for CTL this algorithm was quite intuitive, so you use your original system and then you

label states with information about which sub-formulas are satisfied in these states.

This is appropriate as the sub-formulas are actually evaluated in states, so CTL always

evaluates in states and not on paths, but for LTL we have a different story.

For LTL the sub-formulas are somehow evaluated along a path and not in single states of the

system.

So therefore we need a different approach.

There are a few different model checking algorithms for LTL, but they all share some basic methodology.

So there's a basic strategy that is always employed in these algorithms and we are going

to talk about one of these algorithms in detail.

So we have a model which consists of a transition system, the labeling function and the transition

relation state set and some state in which we want to evaluate the LTL formula, which

I call phi.

So we actually want to determine whether this phi holds in the state s in the system.

So what we are going to do is we are going to construct an automaton and you all know

finite state automaton, automata from other lectures probably and we are going to construct

a slightly different automaton so the technical term would be a generalized non-deterministic,

well GNBA in short, I don't know what the B stands for at the moment, we would have

to look it up, which doesn't accept just words, but it accepts traces.

So a trace would be a sequence, an infinite sequence of valuations for the variables that

we have.

And for a path pi, such an automaton would accept this trace of pi, so the sequence of

variable valuations that you can read off this path if and only if the formula not phi

is satisfied on this path.

And then we are combining this automaton that we obtained with our original model.

So this automaton will look similar to the original model, we can overlap these two and

then pull away all the transitions that don't occur in both systems and all that's left

are paths that simultaneously satisfy not phi and are present in our model.

So all we need to do is find some path in the combined system that starts in a state

that is derived from the original state s that we want to start with.

If such a path exists, then of course ms satisfies phi because there is a path that, wait, is

it the wrong way around?

Yes, it's actually, oh no, no, it's correct, right.

So no, it's the wrong way around.

So if no such path exists, there should be a no here.

So if no such path exists, then we have found no path that satisfies not phi and is present

in the model.

So the original property is satisfied and if we find a path, then we can say no, the

system in state s doesn't satisfy phi and we can read off the counter example from this

very path that we found.

So let's check this out with a really concrete example.

So there's a very simple model in new SMV which has just two variables, Boolean variables

a and b and a transition relation given by these two case distinctions.

And what we want to check is whether this model satisfies not a, u, b, so a should hold

until b is true.