<p>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.</p>

<p>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.</p>

<p>You can start from <a href="http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf">this survey</a> for citations.</p>

CC BY-SA 3.0
2015-01-09T12:41:29.100Z
Thanks, that answers my main question (+1). Since I am interested in the memory requirements of that specific algorithm, I do not need to know whether less memory via better encoding is possible.
DaveBall aka user750378
CC BY-SA 3.0
2015-01-09T12:43:58.920Z
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.
DaveBall aka user750378
CC BY-SA 3.0
2015-01-09T12:50:28.597Z
Oh, the reference is just for the P-completeness. It's unlikely that it will define L and NL. See [here](http://en.wikipedia.org/wiki/NL_%28complexity%29).
P-completeness entails that the space complexity is unlikely to be lower, and as for the space complexity of the algorithm - you can always bound it by the runtime, so it's trivial.
Shaull
CC BY-SA 3.0
2015-01-09T13:24:00.383Z
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!?
DaveBall aka user750378
CC BY-SA 3.0
2015-01-09T13:33:54.943Z
Without getting into too much details of complexity theory - in this case the algorithm is linear in the size of the formula, the number of states, and the number of transitions. Since the algorithm actually traverses the states and transitions many times, it is unlikely that you can reduce any of the arguments. But theoretically - sure, there could be such an algorithm.
Shaull
CC BY-SA 3.0
2015-01-09T16:31:20.947Z
Thanks again for helping, Shauli :) I understand that the time complexity depends on both $\mathit{numberOfStates}$ and $\mathit{numberOfTransitions}$ since the states and transitions are traversed many times. But if the state space is given implicitly, why can CTL MC not be performed with space complexity in $O(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize})$ (or maybe  $O(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize} + ld(\mathit{numberOfTransitions}))$)? This holds at least for the Tarjan SCC sub-algorithm...
DaveBall aka user750378
CC BY-SA 3.0
2015-01-09T16:35:27.470Z
Since you're talking about sub-linear complexity, the whole discussion is a bit problematic, since you can't use an arbitrary computational model such as a RAM machine, you actually need to consider a TM with input, work, and output tapes. Under this model, the space will probably indeed depend logarithmically on the transitions, but it will change the time complexity analysis.
Shaull
CC BY-SA 3.0
2015-01-10T09:27:39.300Z
Oh, then I misunderstood - I thought $O(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize})$ would still be linear. So you are saying CTL MC cannot have $\Theta(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize} \cdot \mathit{numberOfTransitions})$ time complexity and at the same time $\Theta(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize} \cdot ld(\mathit{numberOfTransitions}))$ space complexity!? Because to me, the cited algorithm seems to have those complexities if you smartly iterate over the transitions.
DaveBall aka user750378
CC BY-SA 3.0
2015-01-10T09:35:17.430Z
It's possible (even likely) that the space complexity is lower than the time complexity, but not vice-versa (at least not in a standard TM model).
Shaull
CC BY-SA 3.0
2015-01-09T12:30:59.610Z
2015-01-09T12:30:59.610Z
Shaull
<p>What is the space complexity of the CTL model checking algorithm via labeling without fairness (see e.g. <a href="http://rads.stackoverflow.com/amzn/click/0262032708" rel="nofollow">Model Checking by Clarke at al</a> Section 4.1 or <a href="http://rads.stackoverflow.com/amzn/click/026202649X" rel="nofollow">Principles of Model Checking by Baier et al</a> Section 6.4) that has time complexity $O(\mathit{propertyFormulaSize} \cdot (\mathit{numberOfStates} + \mathit{numberOfTransitions}))$? </p>

<p>Is there a citable reference?</p>

<h3>Details</h3>

<p>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}))$?</p>

<ds.algorithms><model-checking><space-complexity>
What is the space complexity of CTL model checking?
DaveBall aka user750378
# What is the space complexity of CTL model checking?

(Asked by: username_0 on 2015-01-09)

What is the space complexity of the CTL model checking algorithm via labeling without fairness (see e.g. [Model Checking by Clarke at al](http://rads.stackoverflow.com/amzn/click/0262032708) Section 4.1 or [Principles of Model Checking by Baier et al](http://rads.stackoverflow.com/amzn/click/026202649X) 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}))$?

**Tags:** ds.algorithms, model-checking, space-complexity

---

## 1 answers

### Answer by username_1 on 2015-01-09. Score: 5

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](http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf) for citations.

> **Comments:**
> **username_0**: Thanks, that answers my main question (+1). Since I am interested in the memory requirements of that specific algorithm, I do not need to know whether less memory via better encoding is possible.  
> **username_0**: 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.  
> **username_1**: Oh, the reference is just for the P-completeness. It's unlikely that it will define L and NL. See [here](http://en.wikipedia.org/wiki/NL_%28complexity%29). P-completeness entails that the space complexity is unlikely to be lower, and as for the space complexity of the algorithm - you can always bound it by the runtime, so it's trivial.  
> **username_0**: 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!?  
> **username_1**: Without getting into too much details of complexity theory - in this case the algorithm is linear in the size of the formula, the number of states, and the number of transitions. Since the algorithm actually traverses the states and transitions many times, it is unlikely that you can reduce any of the arguments. But theoretically - sure, there could be such an algorithm.  
> **username_0**: Thanks again for helping, Shauli :) I understand that the time complexity depends on both $\mathit{numberOfStates}$ and $\mathit{numberOfTransitions}$ since the states and transitions are traversed many times. But if the state space is given implicitly, why can CTL MC not be performed with space complexity in $O(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize})$ (or maybe  $O(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize} + ld(\mathit{numberOfTransitions}))$)? This holds at least for the Tarjan SCC sub-algorithm...  
> **username_1**: Since you're talking about sub-linear complexity, the whole discussion is a bit problematic, since you can't use an arbitrary computational model such as a RAM machine, you actually need to consider a TM with input, work, and output tapes. Under this model, the space will probably indeed depend logarithmically on the transitions, but it will change the time complexity analysis.  
> **username_0**: Oh, then I misunderstood - I thought $O(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize})$ would still be linear. So you are saying CTL MC cannot have $\Theta(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize} \cdot \mathit{numberOfTransitions})$ time complexity and at the same time $\Theta(\mathit{numberOfStates} \cdot \mathit{propertyFormulaSize} \cdot ld(\mathit{numberOfTransitions}))$ space complexity!? Because to me, the cited algorithm seems to have those complexities if you smartly iterate over the transitions.  
> **username_1**: It's possible (even likely) that the space complexity is lower than the time complexity, but not vice-versa (at least not in a standard TM model).  

---

