计算树逻辑

计算树逻辑（CTL）是一种分支时间逻辑，意味着它的时间模型是一个树状结构，其中未来是不确定的；未来有不同的路径，其中任何一条都可能是实现的实际路径。它被用于软件或硬件工件的形式化验证，通常由被称为模型检查器的软件应用程序来确定一个给定的工件是否拥有安全或活泼属性。例如，CTL可以规定，当某些初始条件得到满足时（例如，所有的程序变量都是正的，或者高速公路上没有汽车跨越两条车道），那么程序的所有可能的执行都会避免一些不理想的情况（例如，一个数字除以0或者两辆车在高速公路上相撞）。在这个例子中，安全属性可以由一个模型检查器来验证，该检查器会探索所有可能的、满足初始条件的程序状态的转换，并确保所有这些执行都满足该属性。计算树逻辑属于一类时间逻辑，包括线性时间逻辑（LTL）。尽管有些属性只能在CTL中表达，有些属性只能在LTL中表达，但在这两种逻辑中可表达的所有属性也都可以在CTL*中表达。

CTL的形式良好的公式语言是由以下语法生成的。CTL使用原子命题作为它的构建模块，对系统的状态进行陈述。然后，这些命题通过逻辑运算符和时间运算符被组合成公式。

逻辑操作符是常用的。¬,∨,∧,⇒和⇔。除了这些运算符之外，CTL公式还可以使用布尔常数true和false。

时态运算符有以下几种。路径A上的量词Φ-全部。Φ-全部：Φ必须在从当前状态开始的所有路径上成立。EΦ-存在：至少有一条从当前状态开始的路径上Φ成立。特定路径的量词Xφ-下一个：Φ必须在下一个状态上成立（这个算子有时被称为N而不是X）。Gφ-全局：φ在整个后续路径上必须成立。Fφ-最后：φ最终必须成立（在后续路径的某个地方）。φUψ-直到：φ必须至少成立，直到在某个位置ψ成立。这意味着ψ将在未来得到验证。φWψ-弱的直到：φ必须持有，直到ψ持有。与U的区别是，不能保证ψ会被验证。在CTL*中，时间运算符可以自由混合。在CTL中，算子必须总是分成两组：一个路径算子后面是一个状态算子。请看下面的例子。CTL*在严格意义上比CTL更具表现力。

在CTL中，有最小的运算符集。所有的CTL公式都可以被转换为只使用这些运算符。这在模型检查中是很有用的。一个最小的运算符集是。{true,∨,¬,EG,EU,EX}。一些用于时态运算符的转换是。