What is the space complexity of CTL model checking? What is the space complexity of the CTL model checking algorithm via labeling without fairness (see e.g. Model Checking by Clarke at al Section 4.1 or Principles of Model Checking by Baier et al Section 6.4) that has time complexity $O(\mathit{propertyFormulaSize} \cdot (\mathit{numberOfStates} + \mathit{numberOfTransitions}))$? 

Is there a citable reference?

Details

Is the space complexity of this algorithm $\Theta(\mathit{numberOfStates} \cdot (\mathit{propertyFormulaSize} + \mathit{numberOfTransitions}))$ or smaller, e.g. $\Theta(\mathit{numberOfStates} \cdot (\mathit{propertyFormulaSize} + \mathit{ld}(\mathit{numberOfTransitions})))$ by smartly iterating over the transitions without storing them while sustaining time complexity $O(\mathit{propertyFormulaSize} \cdot (\mathit{numberOfStates} + \mathit{numberOfTransitions}))$?
In general, CTL model checking is P-complete. Since we think that $L\neq P$ (and moreover $NL\neq P$), it is unlikely that an algorithm with logarithmic space exists. It is also unlikely that a sub-polynomial space algorithm exists, for similar reasons of common belief.

I don't know of exact space-optimizations for the problem, but in general - yes, you need to mark each state with a formula, so naively you need the size you suggest. It may be the case that you can reduce the formula by encoding it more succinctly, but it hasn't attracted attention in research.

You can start from this survey for citations.