时序逻辑在模型检测中被用以描述系统属性，计算树逻辑（Computation TreeLogic,简称CTL）和线性时序逻辑(Linear-timeTemporal,简称LTL)。CTL和LTL的详细介绍，我在这里就不多说了。有个有趣的问题，就是CTL和LTL是否等价，乍一眼看上去似乎LTL里的
时序逻辑在模型检测中被用以描述系统属性，计算树逻辑（Computation TreeLogic
阅读背景：
CTL公式AF、AG与LTL公式F、G等价么…
来源：互联网
分享到：
