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

1.6k comments

538 users

0 votes

Is Local modelling solution unique? Like in my solution I have given precedence to & operator so I splitted on (a |b) and (diamond of x) but the given solution do otherwise? can both be the solutions of only the provided one is correct? If only provided one is correct then isn't it contradicting operator precedence?

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

1 Answer

0 votes
The solution of local model checking is not unique, since there are AND and OR rules. For the OR rules, it is sufficient to choose one subgoal for proving the formula, and for the AND rules it is sufficient to choose one subgoal for disproving the formula. Depending on these choices, we may get different solutions. Apart from that, you may also choose one of the initial states to disprove the formula.
by (166k points)
Thanks for explanation. As you have pointed out the precedence of operators in another post, here I wonder why OR has been evaluated in the given solution first? Should'nt be (a |b) AND (diamond of x)?
No, since AND binds stronger than OR, we have the formula nu x.(a|(b&<>x)).

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
asked May 29, 2020 in * TF "Emb. Sys. and Rob." by nafisur (300 points)
Imprint | Privacy Policy
...