程序逻辑中的区间时序逻辑（ITL） 区间时序逻辑（Interval Temporal Logic, ITL）是一种用于描述有限区间上行为和属性的时序逻辑。与线性时序逻辑（LTL）关注无限轨迹不同，ITL的区间是有限的，适合对程序片段、硬件周期或有限任务进行规约。其核心思想是将时间建模为离散的、有限的区间，并在这些区间上定义逻辑运算符。 基本语法与语义 ITL的公式在给定区间上被解释。设区间是一个有限状态序列 σ = s₀ s₁ ... sₙ，长度为 |σ| = n+1。原子命题包括状态命题（如 x=1）和区间命题（如 empty 表示区间长度为0）。基本运算符包括： 布尔运算符：¬, ∧, ∨ 等。 时序运算符： ○ （next）：○A 在区间 σ 上成立，若 |σ|≥2 且 A 在子区间 s₁...sₙ 上成立。 ; （chop）：A;B 在 σ 上成立，若存在 k（0≤k≤n），使得 A 在 s₀...sₖ 上成立，且 B 在 sₖ...sₙ 上成立。这表示将区间“切分”为两部分分别满足 A 和 B。 ✳ （chop-star）：A✳ 表示区间可被划分为零个或多个连续子区间，每个都满足 A，类似于正则表达式中的 Kleene 星。 表达能力与典型公式 通过 chop 运算符，ITL 可以描述区间上的复合操作。例如： skip ≡ empty ：表示空操作（区间长度为0）。 A⁺ ≡ A;A✳ ：表示 A 重复至少一次。 响应性：“若 P 在区间初成立，则最终 Q 成立”可写为 (P → ◇Q) ，其中 ◇Q ≡ true;Q（存在后缀区间满足 Q）。 扩展与应用 ITL 可通过变量和赋值扩展为可执行规约语言（如 Tempura）。例如，引入变量 len 表示区间长度，或 fin A 表示 A 在区间末尾成立。在程序验证中，ITL 用于规约硬件电路的单周期行为或软件循环的不变式。其模型检测算法通常基于区间枚举或自动机转换。 与其它逻辑的关系 ITL 的区间模型不同于 LTL 的无限路径，但可通过添加无限区间扩展。它与区间逻辑（如 Duration Calculus）共享区间切分思想，但 ITL 更侧重离散时序。chop 运算符的引入使得 ITL 能直接描述顺序组合，与程序逻辑中的序列操作自然对应。