Exam 2020 6b)

Question

How does one come up with these traces and how do they work? I couldn't find any information about this in the lecture slides.

Does the "111 111111111" from q0 and q1 mean that we essentially "spam" a and b (and q1 also c, because we would usually need c to satisfy "strong until c")? How do you know if there is also a c in q1 or not?

Also why is only comparing q1 and q3 sufficient?

Answer 1

The vertical column is the time, each line described the signal on a different variable or formula. So first step, we have b, second a, third a,c, and then repetitively b, followed by a, followed by a,c …

Somebody claims that two formulas are different. We call them q1 and q3, which q0, q2 being their subformulas.

[a SU b] means that we need to have be after finitely many steps. The way to there shall be covered by a in every step. The path starting from the first, fourth, (n*3+1)th position already starts in b, so [a SU b] is statisfied here. Steps 3,6,(n*3) satisfy a but not but b. Also that satisfies [a SU b] already as their successor satisfies b. Step 2, 5, (n*3)+2 satisfy a but not b. As their successor's successor satisfies b, and the step in between satisfies a, they satisfy [a SU b] as well.

That's why we write 111 111 … in the line of [a SU b]. Same thing for [q0 SU c]. We satisfy c at most after two steps. So from every step on [q0 SU c] is satisfied.

The signal traces in the line of q1 and q3 were obtained from the same input traces. As q1 and q3 differ, we know that the formulas are not equivalent.

Comments

Why does q2 = 001 001... satisfy b SU c?
As I understand it, c comes at every 3rd step. Until then, b must be true. But since b never comes and c is not true in the first time step, b SU c should be false?

---

You are right. In step 2 we don't have neither b nor c, and in step 1, we only have b. So in step 1 and 2, [b SU c] is not satisfied. However in the third step, we immediately have c. And all the zero steps up to that point, we had b. That's why we write 001.

Answer 2

The given traces for the variables correspond with a single path, and you should evaluate the LTL formulas on that path as far as possible (since we just see a prefix of the path). To this end, you just have to check the conditions that define when a formula like [a SU b] holds on a path at a certain position t. That is defined on slide 13, and for other operators on slide 16 of the temporal logic chapter. 

Don't know what you mean with "spam" here.

Looking at the recursion laws of the temporal operators, e.g.,

• [a SU b] = b ⋁ a ∧ X[a SU b]
• [a WU b] = b ⋁ a ∧ X[a WU b]

You know that if b holds, we have [a SU b], and if !a&!b holds, then we have ![a SU b], and if we have a&!b, then we have [a SU b] = X[a SU b].

Comments

I know that if b holds, a SU b is satisfied, but why do we then even need a? Because 101 would be b and c where b satisfies a SU b before c which then should satisfie (a SU b) SU c as of my understanding?

Also for me according to this logic b SU c wouldn't be satisfied in q2 for 001? Because 001 would then mean that for the first time steps neither b nor c is true, right? Actually c could never be true in the first and second timesteps at all. Or do we need to consider all these three timesteps together so that just c is true "from the beginning"? But then we could also satisfy a SU b with only b and (a SU b) SU c with only c?

---

Well. If we want the subformula [a SU b] to be satisfied in the second and third step (where we don't have b), then the only option is to have a in the second and third step. In the fourth step, we have b. Hence, the whole formula is satisfied.

About [b SU c]: No, 001 doesn't mean that neither b nor c may be satisfied in the first and the second step. It just means that you may not have a uninterrupted sequence of b ended by c from the first nor from the second step.