 is bounded by $O(n\cdot m^0)$. For CTL, the length is bounded by $O(k\cdot n\cdot m^0)$. In here, $k$ is the number of CTL operators in the formula to be verified, $n$ is the state number in the host system, and $m$ is the state number in the component.  The 