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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes
Question paper for 06.09.2022,
1. Problem 4a (local model checking), how do we split for (a|b->[]x)?

1. Problem 4b (global model checking), how do we get the states for (a|b->[]x)?
in * TF "Emb. Sys. and Rob." by (160 points)

1 Answer

+1 vote
 
Best answer
An implication p->q is just an abbreviation for !p|q, so that we can use the rules for the latter.  However, there were brackets missing in the example solution that I have now added, maybe that was confusing for you. Please check again!

The same answer could be given for global model checking. Hence, States(p->q) = States(!p|q) = States(!p)∪States(q) = (S\States(p))∪States(q).
by (170k points)
selected by
Imprint | Privacy Policy
...