时态逻辑出现在何处

　　这样的断言超出普通断言语言的表示，但可以用形式体系和工具来表示这种语句。我们将这种形式体系称为 时态逻辑。

　　已定义的时态逻辑

　　时态逻辑是一种 模态逻辑，用于推理随时间而更改的特性。

　　请始终记住，有两种常规的时态逻辑：

　　?把未来当作为事件的线性序列的模型

　　?把未来当作为具有各种可能性的树型分叉的模型

　　在本文中，我们将只考虑把未来当作为事件的线性序列模型的时态逻辑。（“分叉树”逻辑非常酷，但它在计算上很难处理。）

　　通常，时态逻辑构建于一组更简单的原子（小单元）命题之上，如传统程序断言。于是，各种模态操作符都可以应用于这些原子断言以生成更复杂的断言。传统的布尔逻辑操作符（如 与(and) 或 或(or) ）可应用于这些断言以生成甚至更复杂的断言。新生成的断言仍可以生成更复杂的断言，并且可以无限地生成下去。

　　时态逻辑使用三个（或四个，取决于模型）常见的模态操作符。

　　典型的模态操作符

　　通常，下列模态操作符可用于时态逻辑：

　　?Always

　　?Sometime

　　?Until

　　?Next （特殊情况）

　　当应用于断言时， Always 确保断言在整个程序执行的剩余部分继续保持。

　　从意义上说，操作符 Sometime 与 Always 是亲戚，但弱得多。当应用于断言时， Sometime 规定一定要在程序执行的今后时间内存在某些断言可以起作用的时间点。

　　Until 应用于两个断言，它规定一旦第一个断言停止作用，此后，第二个断言就必须保持有效。

　　当时间可以是由一系列不连续步骤（比如，程序执行期间）组成的模型时，您有时候会看到 Next 操作符被添加到这个着名的列表中。当 Next应用于断言时，它规定断言在“下一个”步骤中保持有效。当然，仅当我们将时间分割成不连续步骤时，这才有意义。

　　清单 1 显示了一些时态逻辑断言示例：

　　清单 1. 样本时态逻辑断言

　　Always x != 0

　　Sometime x == 0