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


524 users

0 votes


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?.

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

1 Answer

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

Related questions

Imprint | Privacy Policy