Exam 2016.09.06

Question

Hi,

I have two Issues regarding the above question.

• Do we have any simplification rules for handling Bi-implication with state formulas e.g. here we have AG(X(Back_arrow)a <-> a). How do we simplify this?
•  Will X(Back_arrow) a hold for the path which never has a = True? e.g X(!a,....!a)

Thanks,

Answer 1

1. I find the bi-implication simple enough in this case. But you can always write it either as a conjunction of two implications or as a disjunction of the two case: some ↔ thing = (some → thing) ∧ (thing → some) = (some ∧ thing) ∨ (¬some ∧ ¬thing)
2. Yes. It holds in the first step. Everything is true before the beginning of time.

Answer 2

We do not have special simplification rules for the equivalence operator. You have to expand it to a DNF or CNF for simplifications that you have in mind.

The X(back-arrow) is the previous operator, and in the case above, it is the weak version. It holds, if "a" holds at the previous point of time if there is one. The strong previous operator is false at initial time while the weak one (that you have here) is initially true.