6.4 符号模型检验 6.4.3 基于时态逻辑的计算树逻辑CTL 　符号模型检验用计算树逻辑CTL来描述需要验证的性质。CTL是基于时态逻辑（Temporal logic）发展而来的。下面我们先简要介绍一下时态逻辑。 　1. 时态逻辑TL