Precedence Level of Operators in Local Model Checking

Question

Hi,

I have one issue regarding the precedence level of operators in Local Model Checking. 

• Do we just solve from left to right regardless of precedence level?
• Do we solve in regard to precedence level?.

Answer 1

No, we do not just solve it from left to right and instead follow the precedences. The precedences are the same throughout the course. Conjunctions binds stronger than disjunction, and since local model checking works in a top-down manner, disjunction comes first here.

Comments

thanks, could you explain "top-down manner " a bit?

---

If you consider the syntax-tree of the formula, top-down means working from the root node downwards to the leaf nodes.

---

okay in the given example a is considered as a root node?

---

No, the syntax tree I am taking about of the formula a | (b & <> x), so it starts with a root node labeled with disjunction having left child a and right child b&<>x and so on.

---

okay thanks, so in case of e.g s0 |- a & (b <-> <>c) we will have s0 |- a and  s0 |- (b <-> <>c) ?

---

Sure. You may try that with the teaching tool to convince yourself about this.