How is this solution of LTL conversion valid?

Question

φ2 = ¬EFE[1 SU ¬a] ∧ AGA[ a SB b] 

Can you please explain the solution provided here? The extract is from the exam solutions.

The implication in the first step seems to be wrong.

Answer 1

Thank you for this question.

Which exam is this solution from?

Let's talk about the transformations first:

1. [1 SU ¬a] = F ¬a. The strong until requires the right side to hold eventually, and the left side to hold on every step on the way. As 1 is constantly true, and hence trivially satisfied, this is equivalent to F ¬a.
2. EFEF ¬a → … = AGAG a ∨ …. These are actually two transformations. In propositional logic, we introduced the implication as a shortcut for a disjunction with a negation: C → D = ¬C ∨ D. The negated temporal subformula ¬EFEF ¬a can then be simplified to AGAG as the negation flips E to A, F to G, and ¬a to a.
3. AGA[a SB b] = AG[a SB b]. The inner A got dropped as the outer AG already required the inner subformula to hold on every step on every path. The inner subformula A[a SB b] requires the Strong-Before-statement to hold on every path. As the outer formula required this inner formula to hold on every step on every bath, the A of the inner subformula is redundant.
4. AG[a SB b] = AG (a ∧ ¬b). The inner most temporal formula [a SB b] is satisfied if and only after finitely many steps the literal a holds and b is not seen up this point. As the outer formula requires the inner one to hold on every step, this means that b is forbidden. If there was a b at some point, [a SB b] would not hold there. Also, the formula requires a to hold infinitely often. If there was a point (after finitely many steps) at which a would hold never again, then [ a SB b ] could not be satisfied as the operator is strong.  Here, I do think there's a mistake in the solution!  It says that the literal a has to hold in every single step. In fact, only [ a SB b ] shall hold in every step. This means that in every single step, it only need to be finitely many steps to the next point where literal a holds. You can check this using our LTL tools. G[ a SB b ] <-> G(¬b & F(a)) is valid, while G[ a SB b ] → G(¬b & a) produces a counterexample.
5. AGAG a = AG a. This is a common simplification. The longer formula requires literal a to hold on every state that is reachable from a reachable state, the shorter formula shortens this to just the reachable state which is equivalent.
6. The last line is a misprint. The whole transformations are done assuming that the outer connective is an implication. Here, the outer connective is actually a conjunction. For the two subformulas, one implies the other one, i.e. when one of them holds (the stronger one), the other one (the weaker one) needs to hold as well. In conjunctions, the weaker one can be dropped. In disjunctions, the stronger one can be dropped.

As I said, there seems to be some misprints. If you could tell us which exam/solution this example is from, we can repair this.

Comments

Thanks for your reply Martin.
The question is from the exam taken on 27th August, 2019. Problem 8a part 2. I suggest you to please look at other answers in the same Problem 8 for errors, where it seems there are also some misprints.

---

The other solutions of 8a look fine to me. I realized that the bug in the solution had been fixed long time ago but just hadn't made it to the web. We'll upload the corrected version soon.