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


543 users

0 votes

Does this structure satisfy S2?

For given S2: I tried to consider the next state of the initial state because of X and in the s1 state, I made aSUb true by making the b(the second term in aSUb) globally true.

In the state s0, given S1 doesn't satisfy.

Let me know if my approach is incorrect.

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

1 Answer

+1 vote
Your solution is correct, since you can prove that the following LTL formula is valid:

!a & !b & X G (!a&b) -> X[a SU b] & ![(X a) SU b]
by (166k points)
Thank you, Professor
Imprint | Privacy Policy