程序逻辑中的区间时序逻辑（ITL）

区间时序逻辑是一种时序逻辑，其时间模型是有限或无限的区间，而不是离散的时间点。它允许描述程序在连续时间段内的行为。

1. 基本概念：ITL 的核心是将时间视为区间（interval），即从一个起始时刻到终止时刻的时间段。区间可以是有限的（有明确的起点和终点）或无限的。在 ITL 中，公式的真值是在整个区间上定义的，而不是在单个时间点上。例如，一个公式可能表示“在某个区间内，变量 x 始终大于 0”。

2. 语法：ITL 的公式由以下部分组成：

   • 状态变量（如 x, y）和常量。
   • 逻辑运算符：¬（非）、∧（与）、∨（或）等。
   • 时序运算符：核心是“chop”运算符（记作 ;），它将区间分割为两部分。公式 φ;ψ 表示区间可以分成两个子区间，使得 φ 在前半部分成立，ψ 在后半部分成立。
   • 其他派生运算符：例如，◇（有时）表示区间存在一个子区间满足公式，□（总是）表示所有子区间都满足公式。

3. 语义：ITL 的语义基于区间模型。一个区间由起始时间、终止时间和变量在时间上的赋值函数定义。公式的真值通过区间长度和变量值来判定。例如，□φ 在区间上为真，当且仅当对于该区间的每个子区间，φ 都成立。chop 运算符的语义是：φ;ψ 在区间 [a,b] 上为真，当且仅当存在时间点 c（a ≤ c ≤ b），使得 φ 在 [a,c] 上为真，且 ψ 在 [c,b] 上为真。

4. 应用：ITL 常用于规范和分析持续性的系统行为，如硬件电路（信号在时钟周期内的变化）或实时系统（任务在时间段内的执行）。它可以表达持续时间属性，例如“操作 A 在 5 秒内完成，然后操作 B 开始”。通过扩展，ITL 还可用于程序验证，如证明循环在有限区间内终止。