# 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.
• Thanks for the reference - this morning I googled that survey and searched for space complexity and did not find it in there. Will have a closer look. I guess the document will also define $L$ and $NL$, which are new to me. Jan 9, 2015 at 12:43
• Thanks for your comment, Shauli (+1). Now I better see the connection between the first and second paragraph of your answer. What is the smallest polynomial space complexity when you have multiple parameters like $\mathit{propertyFormulaSize}$, $\mathit{numberOfStates}$, and $\mathit{numberOfTransitions}$? For instance, is $O(\mathit{numberOfStates})$ still polynomial? Then there could theoretically be a smart CTL MC algorithm, e.g. with formula encoding and elaborate pruning, that only requires $O(\mathit{numberOfStates})$ space!? Jan 9, 2015 at 13:24