2
$\begingroup$

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

Improve this question
$\endgroup$

1 Answer 1

Reset to default
5
+50
$\begingroup$

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.

Improve this answer
$\endgroup$
9
  • $\begingroup$ 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. $\endgroup$
    – DaveBall aka user750378
    Commented Jan 9, 2015 at 12:41
  • $\begingroup$ 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. $\endgroup$
    – DaveBall aka user750378
    Commented Jan 9, 2015 at 12:43
  • 1
    $\begingroup$ Oh, the reference is just for the P-completeness. It's unlikely that it will define L and NL. See here. 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. $\endgroup$
    – Shaull
    Commented Jan 9, 2015 at 12:50
  • $\begingroup$ 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!? $\endgroup$
    – DaveBall aka user750378
    Commented Jan 9, 2015 at 13:24
  • $\begingroup$ 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. $\endgroup$
    – Shaull
    Commented Jan 9, 2015 at 13:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.