CTL properties can be checked in linear time (see [Clarke et al][1]).

Long time ago I used to work in a company where many colleagues used [Rulebase][2] to verify integrated circuit designs. The property language is [PSL][3], it is standardized by IEEE, and is a kind of CTL on steroids.


  [1]: http://scholar.google.co.uk/scholar?cluster=326651136244218780
  [2]: http://www.research.ibm.com/haifa/projects/verification/RB_Homepage/
  [3]: http://dx.doi.org/10.1109/IEEESTD.2005.97780