Okay, then let's start.

So last time we realized that our construction from two weeks ago where we constructed automata

for LTL formula yields somehow unnecessarily large automata because in the exercise you

could create a two-state automaton for this A until B formula, whereas the constructed

one had I think five states.

So the question was is this in somehow an optimal algorithm?

So are there formulas that always create an automaton of this size?

And to answer this question we need to expand a bit more on the theory of this whole stuff.

So what I start with is an expansion of the semantics of LTL.

And first we define a notion of words over a formula phi.

So that is just a set of elements of the power set of atoms to the omega.

So I'm not sure if you have seen this notation before.

So it's bracketed like this of course.

So the subsets of our atoms are just valuations.

And this omega here means that we have infinite sequences.

So you could also define it as sigma as a function from natural numbers to power set

of atoms.

And it's constrained by this.

So sigma should also satisfy psi.

And now we have a problem because initially we defined the semantics of LTL formulae using

paths in a model and not using these valuations or traces or whatever you want to call them.

Yeah, well, words as we call them now.

So we need to adapt the semantics.

And the only place where we need to adapt it is so sigma satisfies what?

A variable of course, or a proposition in the Latin, P.

And now in the version from the lecture we had L of something.

So I can write it shortly here.

So L of pi equals P in L of pi.

And now we don't need that because we have these subsets here of our atoms.

And we don't need to project via L, but we can just say, well, if P is in signal.

And the rest of the semantics stays the same.

And then for paths, well, we still do have paths and models and so on.

But for paths we need a definition what a trace is.

So we define it informally in the tutorials.

But now we can just say that a trace of a path pi is just L applied to S0, L applied

to S1, L applied to and so on.

So it's an infinite sequence of exactly these subsets of eight atoms.

So this is also an element of power set atom to the omega.

And then we can generalize this and say trace of a set of paths, which I denote by big pi,

capital pi is the set of all traces for paths in this set of paths, pi in pi.

And for a model, which is just a transition system, we can also define what the trace

is, and now I use the capital of a model R. And that's just, well, trace of all paths

for which pi equals pi 0, pi 1, pi 2, and so on, and pi 0 is initial.

Oh, yes, we can call it state or whatever.

And this leads to another problem because I think we define transition systems without

initial states.

So for our purposes now, transition systems are expanded with initial states.

And additionally, I also mentioned the atoms.

So Tadeusz only said, well, the labeling function is a function from natural numbers

to from states to atoms, but I include this atom set directly in the definition of transition