I'm told the following CTL formulas aren't equivalent. However, I can't find a model in which one is true and the other isn't. CTL is a computational temporal logic.
Formula 1: AF p OR AF q
Formula 2: AF( p OR q )
The first says: For all paths starting from the begin state there is a future in which p holds OR for all paths starting from the begin state there is a future in which q holds.
The second: For all paths starting from the begin state there is a future in which p OR q holds.
The model is a little bit tricky. Firstly, one should note that AF(p OR q) implies AF p OR AF q. So, we are looking for a model in which AF (p OR q) is true but AF p OR AF q is false.
I am assuming that you are familiar with Kripke model notation described in Logic in Computer Science textbook by M. Huth and M. Ryan (see http://www.cs.bham.ac.uk/research/projects/lics/).
Let M = (S, R, L) be a model with S = {s0, s1, s2} as the set of possible states, R = {(s0,s1), (s0,s2), (s1,s1), (s1,s2), (s2,s2)} as the transition relation, and L is a labeling function defined as follows: L(s0) = {} (empty set), L(s1) = {p}, and L(s2) = {q}.
Suppose the starting state is s0. It is clear that AF (p OR q) holds at s0. However, AF p OR AF q is not satisfied at s0. To prove this, we have to show that s0 does not satisfy AF p *and* s0 does not satisfy AF q.
AF p is not satisfied at s0 since we can choose the path s0 -> s2 -> s2 -> s2 -> ...
Similarly, AF q is not satisfied at s1 since we can choose the path s0 -> s1 -> s1 -> s1 -> ...