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

543 users

0 votes

Which rule do we need in local model checking if there is an implication in the formula? 

S1|/- (c | b -> [] x)) can be rewritten to  S1|/- (!c & !b | [] x1)), but the solution splits it into S1|/- (!c & b)) and S1|/- ([]x1). Why is that done this way?

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

1 Answer

+1 vote

Thanks for pointing this out. Some years ago, there was a but in the pretty printer that did not respect the priorities of the operators in the correct way. In state s1, the formula is actually !(c|b) and not !c|b, so that the correct proof tree is as follows:

It has been fixed in the exam paper meanwhile. 

by (166k points)
Imprint | Privacy Policy
...