# LTL and CTL equivalence

I would like to understand the difference between the two formulas. My first attempt to answer this question was trying to satisfy S2 with one of these:

In my understanding, both satisfy S2 and not S1. However, I do not understand how the solution given satisfies S1.

Can someone please clarify?

+1 vote

It looks good! Consider the structure in the example solution:

```             0 1 2 3 4 5 6
a 0 0 0 0 0 0 ...
b 1 0 1 0 1 0 ...
[a SU b] 1 0 1 0 1 0 ...
X[a SU b] 0 1 0 1 0 1 ...
Xa 0 0 0 0 0 0 ...
[Xa SU b] 1 0 1 0 1 0 ...

```

Note that [a SU b] becomes equivalent to "b" if "a" is always false. Thus, the two formulas X[a SU b] and [Xa SU b] just become equivalent to Xb and b, respectively.

Your first structure generates the following

```             0 1 2 3 4 5 6
a 0 1 0 0 0 0 ...
b 0 0 1 1 1 1 ...
[a SU b] 0 1 1 1 1 1 ...
X[a SU b] 1 1 1 1 1 1 ...
Xa 1 0 0 0 0 0 ...
b 0 0 1 1 1 1 ...
[Xa SU b] 0 0 1 1 1 1 ...

```

So, here X[a SU b] holds, and [Xa SU b] is false.

Finally, your second structure:

```             0 1 2 3 4 5 6
a 0 0 0 0 0 0 ...
b 0 1 1 1 1 1 ...
[a SU b] 0 1 1 1 1 1 ...
X[a SU b] 1 1 1 1 1 1 ...
Xa 0 0 0 0 0 0 ...
b 0 1 1 1 1 1 ...
[Xa SU b] 0 1 1 1 1 1 ...

```

Again, here X[a SU b] holds, and [Xa SU b] is false.

by (170k points)
selected by
Thank you very much for the instructive answer! It clarified everything.