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

Can you please explain the rule that led to the step where I placed a Question mark in the image below?

Same with the below question as well.

 

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

1 Answer

0 votes

That rule is explained in detail on slides 45-46 of the temporal logic chapter. There are the following important equivalences that allow us to remove conjunctions of temporal operations by a temporal operator which is sometimes required for a translation to CTL:

  • [a1 SU b1] & [a2 SU b2] = [(a1 & a2) SU (b1 & [a2 SU b2] | b2 & [a1 SU b1])]
  • [a1 SU b1] & [a2 WU b2] = [(a1 & a2) SU (b1 & [a2 WU b2] | b2 & [a1 SU b1])]
  • [a1 WU b1] & [a2 WU b2] = [(a1 & a2) WU (b1 & [a2 WU b2] | b2 & [a1 WU b1])]
Slides 47-49 consider conjunctions with all other temporal operators which are reduced to the above three basic laws.

by (170k points)
Thank you, Professor

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...