# Exam Paper : 2018.08.21 and 2018.02.14

Referring to Exam Paper : 2018.08.21 (Question 8c) and 2018.02.14 (Question 8c) respectively-

In the first question- Isn't it for S2, next state should be where 'a' must be true? So, the structure for S2 could be 'a with a loop'?

A self-loop on a state labeled with a will neither satisfy S1 nor S2 in the first example.  The subformula !a& Xa holds on a path if in a state !a holds and on the successor state a holds. Hence, a must switch from false to true.

The formula a <-> X!a holds whenever there is a change on the truth value of a, i.e., if a switches from false to true as the above formula, but also if a switches from true to false. This is so, since a <-> X!a is equivalent to a&X!a | !a&Xa which contains the former formula. The past version of the X does not make a big difference here.

I guess the latter needs a bit more explanation: Looking at EXF((PWX!a)<->a), we can rewrite this to EFX((PWX!a)<->a) which is equivalent to  EF(!a<->X a)  and that is in turn equivalent to EF((!a&Xa | a&!Xa)), and also to EF(!a&Xa) | EF(a&!Xa) which makes S2 equivalent to S1 | EF(a&!Xa).

In the second case, we have EF((PWX!a)<->a) instead of EXF((PWX!a)<->a) and these two formulas are not equivalent as can be seen by the discussed structures. Note that PWX p holds initially for any p, and since a also holds on the single path in the second structure, (PWX!a)<->a holds initially on that single path, and thus also F((PWX!a)<->a) holds there. However, variable a never changes its value.
by (167k points)
edited by