How was this equation converted to CTL?

Question

In the exam of February 14th, 2024, I understood the first step which distributed A over the two equations due to and operator. But what syntactic sugar was used to solve the rest of the steps? Thank you.

Answer 1

The following equivalences were used step by step:

• A(phi & psi) = (A phi) & (A psi)
• F[a SU b] = F b
• G[a W b] = G(!b|a)
• AF b = mu x.(b|[]x)
• AG(!b|a) = nu y. ((Phi_Inf -> (!b|a))&[]y)