Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


543 users

0 votes


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)

in * TF "Emb. Sys. and Rob." by (1.4k points)

2 Answers

+1 vote
Best answer
  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.
by (25.6k points)
selected by
0 votes
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.
by (166k points)

Related questions

Imprint | Privacy Policy