You can partially evaluate the formula. Note the structure (p' → …) ∧ a. This means that edges only exist with a being true. Also, every state has all possible transitions with variable a being true for successor states where p' is false.
Hence, you can already draw transitions from all states to the half without p, and label the transitions {a}, {a,o}.
Next, we assume that a and p' are true. We then consider the inner formula p ∧ (o ↔ q) ↔ q'. For p being false, the inner biimplication doesn't matter. Just q' needs to be false. So you can add transitions labeled {a} and {a,o} from states without p to the state with p' true, and q' false.
Now we look at the inner biimplication. We assume a, p', p to be true In this case, we need to statisfy (o ↔ q) ↔ q'. If q' is true, the inner biimplication needs to be satisfied; for q' false, the inner bimimplication may not be satisfied. Hence, you add the transitions from all states with p to states with p'. Just be careful with the labels. Add o precisely to the labels of transitions from positive q to positive q' and negative q to negative q'.
Now, we have covered all cases. If you want to do it with care, you can create a partial truth table for a, p, p'.
| p | p' | a | φR |
|---|
| – | – | false | false |
| – | false | true | true |
| false | true | true | ¬q' |
| true | true | true | (o ↔ q) ↔ q' |
