I have a slide that gives the worst case time complexity of LTL model checking which uses a product construction of an LTS along with the NBA for the negation of the LTL formula. enter image description here

My question is, when does this worst case complexity happen, for what LTL formula (its negation) does the corresponding size of the NBA become exponential in the number of operators.

  • $\begingroup$ I don't understand what you are asking or what kind answer you are looking for. I don't know what it means to ask "when does this happen" or how one is supposed to answer that. $\endgroup$
    – D.W.
    Commented May 4 at 3:10
  • $\begingroup$ @D.W. I've edited it, essentially for what LTL formula do we get an NBA that has size exponential in the number of operators $\endgroup$
    – revision
    Commented May 4 at 7:19
  • $\begingroup$ Usually there are infinitely many problem instances that cause an algorithm to hit its worst-case running time. I'm not sure what kind of answer you are expecting or hoping for. $\endgroup$
    – D.W.
    Commented May 4 at 8:37
  • $\begingroup$ @D.W. Just wondering if there are any easy-to-see/interesting examples where this happens $\endgroup$
    – revision
    Commented May 4 at 8:38


Your Answer

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