图6.5为部分CTL时态操作符的语义的直观解释。其中蓝色圆圈表示f为真的状态，红色圆圈表示f为假的状态。
下面是一些典型的 CTL 公式：
· AG ( EF restart )：表示从任何状态总能到达 restart 状态。
· AG (req→AF ack)：表示任何一个请求(req)总能得到响应(ask)。
图6.5 CTL时态操作符的语义解释P6-4-1 |
CTL的特点是：（1）关于路径的特性A和E，是指所有的路径都成立，还是只要有一条路经成立即可。（2）关于某条路经上的状态变量的特性，G指所有的状态，F指路径上的某一状态，X指当前状态的次态，U指在某一状态前的各状态。
CTL的理解与描述相对比较困难，但逻辑体系比较严密，它适合于做研究，适合于系统开发时使用，但不适合于用户描述，好的软件应自动将用户的描述语言描述转换成CTL描述。