Linear vs. branching time: A complexity-theoretic perspective

The discussion of the relative merits of linear versus branching time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that "while specifying is easier in LTL (linear-temporal logic), verification is easier for CTL (branching-temporal logic)". Indeed, the restricted syntax of CTL limits its expressive power and many important behaviors (e.g., strong fairness) can not be specified in CTL. On the other hand, while model checking for CTL can be done in time that is linear in the size of the specification, it takes time that is exponential in the specification for LTL. A closer examination of the the issue reveals, however, that the computational superiority of the branching time framework is perhaps illusory. In this talk we will compare the complexity of branching-time verification vs. linear-time verification in many scenarios, and show that linear-time verification is not harder and often is even easier than branching-time verification. This suggests that the tradeoff between branching and linear time is not a simple tradeoff between complexity and expressiveness.