计算树逻辑Computation Tree Logic(CTL)是一种分支时序时态逻辑(temporal logic of branching time)。这里给出CTL时态逻辑的语法及语义解释。
　　CTL是针对具有分支路径的状态转换图（即计算树）定义的逻辑，因此它的时态操作符表示了有关分支路径的特性。
　　CTL的时态操作符由两个部分组成：一个称为路径量词；后面紧跟一个表示时序的时间操作符。因为实用在计算机中，不用上面用的符号，而用大写字母来表示。其中，路径量词只有两种：A代表适用于所有的计算路径，E代表存在至少一条以上的计算路径。时间操作符共分为四种，分别是：
　　· X："次态 (next time)"操作符，
　　· F："最终 (eventually)"操作符，
　　· G："全程 (globally)"操作符，
　　· U："直到 (until)"操作符。
　　符号A、E等同于常用的符号和，分别读为"所有"和"存在"。符号G、F、X与前面的图形符号□、◇、○相对应。在CTL中，A表示所有路径；E表示至少存在一条路经；Gp表示路径上所有的状态p成立；Fp表示路径上总会有一个状态p成立，意思与存在某一个状态p成立相同；Xp表示路径上下一个状态p成立；[pUq]表示路径上在q成立之前p一直成立。这些运算符都是值当前状态下的后继状态而言的。
　　通过两个路径量词和四种时间操作符的组合，总共是八种CTL时态操作符。下面，首先使用EX，EU和EG这三种最基本的CTL时态操作符给出CTL公式的定义。其它五种CTL时态操作符均可以使用这三种基本操作符进行表示。
　　CTL公式定义：令P为原子命题集合，则CTL公式定义如下：
　　· 对于P中的每个原子命题p（即p∈P）均是CTL公式；
　　· 如果f和g均为CTL公式，则 ┐f，f ∨ g，EX f，E[f U g] 以及 EG f 都是CTL公式。
　　其中 ┐和 ∨ 分别代表布尔逻辑中的"非"操作符和"或"操作符。至于其它的布尔操作符则可以定义为"非"和"或"的表达式。而后三种时态操作符的语义解释如下：
　　· EX f：在当前状态的某些后继状态中f 成立。
　　· E[f U g]：对于从当前状态开始的某些计算路径，在其路径中存在一个状态满足g，并且在该状态之前所有的状态都满足f。
　　· EG f：存在一条路径，且该路径上的每个状态都满足f。
　　其它五种描述时序行为的 CTL 操作符用上述三种操作符表示如下：
　　· AX = ┐EX┐f：在当前状态的所有后继状态中f都成立。
　　· EF f = E[ true U f]：对于从当前状态开始的某些计算路径，在其路径中存在一个满足f 的状态。
　　· AF f = ┐EG┐f：对于从当前状态开始的所有计算路径，在其路径中都存在一个满足f 的状态。
　　· AG f = ┐EF┐f：每条路径上的每个状态都满足f。
　　· A[ f U g] = (┐E[┐g U (┐f ∧┐g)]∧(┐EG┐g)：对于从当前状态开始的每条计算路径，在其路径中都存在一个状态满足g，并且在该状态之前所有的状态都满足f 。