Differenza tra equivalenza e implicazioni

Question

In termini di formule CTL, qual è la differenza tra equivalenza e implicazioni?

(Prop = qualche proposta, && = Congiunzione, Ag = Sintassi CTL per "Holds a livello globale")

EG AG (prop1 && prop2) contro (ag prop1) && (ag prop2)

Quelle due formule sono correlate per implicazione, cioè il lato sinistro implica il lato destro? O sono davvero equivalenti?