To prove that [a SU b] | [!a WB b] is valid, we prove that its negation !([a SU b] | [!a WB b]) is unsatisfiable. To this end, we translate the latter to an equivalent omega automaton and prove that it cannot accept any word.
To translate !([a SU b] | [!a WB b]) to an omega-automaton, we abbreviate the subformulas [a SU b] and [!a WB b] with state variables q0 and q1, respectively, so that the formula becomes our initial state formula !(q0 | q1). Next, we have to add transition relations and acceptance conditions so that q0 and q1 behave exactly as [a SU b] and [!a WB b], respectively.
Slide 72 of the temporal logic chapter tells us the following
- G[q↔[φ SU ψ]] ⇔ G[q↔ψ∨φ∧Xq]∧GF[q→ψ]
- G[q↔[φ WB ψ]] ⇔ G[q↔¬ψ∧(φ∨Xq)]∧GF[q∨ψ]
Instantiated for our case, this becomes
- G[q0↔[ a SU b]] ⇔ G[q0↔b∨a∧Xq0]∧GF[q0→b]
- G[q1↔[!a WB b]] ⇔ G[q1↔!b∧(!a∨Xq1)]∧GF[q1∨b]
Hence, the omega-automaton has the transition relation (q0↔b∨a∧Xq0) ∧ (q1↔!b∧(!a∨Xq1)) and the acceptance condition GF[q0→b] ∧ GF[q1∨b] so that it looks finally as follows:
AUTOexists(
{q0,q1},
!(q0∨q1)
(q0↔b∨a∧Xq0) ∧ (q1↔!b∧(!a∨Xq1)),
GF[q0→b] ∧ GF[q1∨b]
)
That above automaton is fine as it is, and could be used as it is. Since q0 represents a strong operator and has a negative occurrence, we may however neglect the acceptance condition GF[q0→b] since it is redundant (see slides 81 and following). Hence, we may simply use
AUTOexists(
{q0,q1},
!(q0∨q1)
(q0↔b∨a∧Xq0) ∧ (q1↔!b∧(!a∨Xq1)),
GF[q1∨b]
)Having explained all that, I have to mention that the above procedure is explained in full detail on the slides in the chapter about temporal logics, and a couple of examples are presented there also. You should have read and understood that before looking at exercises. Have you read it already?
That part of the exercise is just the application of the standard translation which is straightforward. The remaining part is more interesting since it remains to check that the above automaton does not accept any word. To that end, you have to check that no path starting in an initial state can satisfy GF[q1∨b].
