0 votes

for the question 3 c 

we can see that SIM3 does not hold for Q0 of k2 in the step 0 . So can I just conclude from this step that k2<k1 does not hold or do I have to perform the SIM 1 and SIM 2 check ?

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

1 Answer

+1 vote
Yes, that would be a valid answer if you give some reason for your claim. For instance, the following could be accepted:

K2<=K1 cannot hold, since finally, every initial state of K2 must be simulated by an initial state of K1. However, the initial state q0 of K2 has label {d}, but none of the initial states of K1 have that label. Hence, no initial state of K1 can simulate the initial state q0 of K2, and thus, K2 is not simulated by K1.
by (92.2k points)
Imprint | Privacy Policy
...