# CTL, LTL and CTL*

1. S1 = EF((X(a → b)) ⊕ (a → b))

S2 = EF((a ∧ ¬b) ∧ X(a → b))

Can I draw a path with

with states s0(initial state) and s1 with b in s0 and a in s1 with an infinite loop on s1 ? I am guessing this would satisfy S1 but not S2 since state s0 has a in it?

2.  S1 = ¬XX (G(a ⊕ b) ⊕ F(a ↔ b))

S2 = XXG((a ⊕ Xa) ∧ (b ⊕ XXb))

Can I draw a path with states s0 (initial state), s1 and s2. Both states s0 and s1 are empty and s2 has {a,b} in it with an infinite loop. I believe this will satisfy S2 since S1 is always false.

3. S1 = c ∧ F [b U G(¬a ↔ Xa)]

S2 = c ∧ [(Fb) U G(¬a ↔ Xa)]

Can I draw a path with states s0 (initial state), s1 and s2. State s0 has c, s1 is empty and s2 has {a} with an infinite loop. (in the exam solutions states s1 and s2 have an alternating loop. Is it alright if I draw an infinite loop on s2?) I believe it would still satisfy S1 and not S2.

If you have a Kripke structure with just one infinite path, then the path quantifiers don't matter, i.e., E and A become the same, and you can express that in LTL as well. For example, you can check whether your ideas are right as follows using the LTL prover:

First example:

```    S1 = EF((X(a → b)) ⊕ (a → b))
S2 = EF((a ∧ ¬b) ∧ X(a → b))
```

You can prove the following to see that you are right:

```    (!a&b) & (X G(a&!b)) -> F((X(a → b)) ⊕ (a → b))
(!a&b) & (X G(a&!b)) -> !F((a ∧ ¬b) ∧ X(a → b))
```

and you can see that also with the following traces:

```                            a : 01...
b : 10...
a → b : 10...
X(a → b) : 00...
a ∧ ¬b : 01...
(X(a → b)) ⊕ (a → b) : 10...
(a ∧ ¬b) ∧ X(a → b) : 00...
```

Second example: First note that G(a⊕b) = ¬F(a↔b), hence, G(a⊕b) ⊕ F(a↔b) is true, so that S1 is always false and we focus on satisfying S2 = XXG((a ⊕ Xa) ∧ (b ⊕ XXb)). I think that you are wrong due to the following traces:

```                a : 00 11
b : 00 11
Xa : 01 11
a⊕Xa : 01 00
XXb : 11 11
b⊕XXb : 11 00
(a⊕Xa)∧(b⊕XXb) : 01 00```

Third example: I guess these were SU (?):

```    S1 = c ∧ F[b SU G(¬a ↔ X a)]
S2 = c ∧ [(F b) SU G(¬a ↔ X a)]

a : 00 11
b : 00 00
c : 10 00
Xa : 01 11
¬a↔Xa : 01 00
G(¬a↔Xa) : 00 00
```

and thus the SU will be false.

by (148k points)