时间自动机

控制位置与时钟估值 ​

时间自动机由有限位置集合 $L$、时钟集合 $X$、边和位置不变量组成。时钟估值是函数

$$v:X\to {\mathbb{R}}_{\ge 0},$$

使用非负实数公理库实数系Real number system · Ordered complete field满足序域公理与上确界完备性的数系。记录自上次 reset 后经过的时间。状态是 $(\ell ,v)$，控制位置有限，估值空间却不可数无限。

边写作

$$\ell \stackrel{a,g,R}{\to }{\ell }^{\prime },$$

其中 $a$ 是动作，guard $g$ 是形如 $x\bowtie c$ 或 $x-y\bowtie c$ 的时钟约束，$R\subseteq X$ 是触发后重置为零的时钟集。

它扩展有限状态自动机公理库有限状态自动机Finite-state automaton · Finite automaton · Finite-state machine以有限状态压缩输入前缀信息、沿带标号转移读取有限字的通用自动机骨架。的离散控制，但不是给每条边附一个固定耗时；时间可以在位置中连续流逝。

两类转移 ​

delay 转移

$$(\ell ,v)\stackrel{d}{\to }(\ell ,v+d),d\ge 0$$

要求整个延迟区间内都满足位置 invariant $Inv(\ell )$。离散转移要求 $v\models g$，重置 $R$ 后的新估值满足目标位置 invariant。

位置 invariant 例如 $x\le 5$ 会禁止在该位置停留超过五个时间单位；guard $x\ge 2$ 则禁止动作过早发生。二者共同给出允许窗口。

若只检查延迟终点满足 invariant，而中间可能违反非凸约束，会错误允许时间穿过非法区域；标准 timed automata 通常使用适合连续检查的时钟约束。

超时协议轨迹 ​

请求进入 waiting 时 reset 时钟 $x:=0$。收到响应的边 guard 为 $x\le 3$，超时边 guard 为 $x>3$。

一条正常轨迹是

$$(idle,0)\stackrel{request}{\to }(waiting,0)\stackrel{2.4}{\to }(waiting,2.4)\stackrel{reply}{\to }(done,2.4).$$

若 waiting invariant 设为 $x\le 3$，则系统在 $x=3$ 必须采取某条离散边；但超时 guard 若错误写成 $x>3$，在边界 $x=3$ 没有动作可走，产生 time-lock。guard 与 invariant 的开闭端点必须协同。

时间自动机的非确定性允许多个边窗口重叠。它不表示在重叠区间平均随机选择，也不自动采用“最早事件优先”。

若位置允许任意延迟，动作即使从 $x=1$ 起使能也可一直不执行，直到 invariant 边界。要表达 urgent action，可让位置 invariant 迫使时间停止，或使用工具提供的 urgent/committed 语义；两种机制对其他组件是否还能交错可能不同。

输入动作的时间常由环境决定，输出动作由系统决定。验证 controllability 或 timed games 时需区分两类选择；普通可达性把它们都当非确定边，无法回答控制器是否能保证 deadline。

区域等价 ​

设模型中最大整数常数为 $M$。区域抽象只记录：每个时钟整数部分是否超过 $M$、小数部分是否为零，以及各时钟小数部分的相对次序。

满足同一区域的估值对未来 guard/reset 行为不可区分，因此有限多个区域构成 time-abstract bisimulation。可达性由此归约到有限 region graph。

区域数对时钟个数呈指数/阶乘增长，理论上有限却常不适合直接实现。它证明可判定性，不保证实际状态空间小。

region equivalence 保存 untimed action sequence 与时钟约束可达性，不保存每条运行的精确延迟。若性质询问累计时间、最小延迟或成本，需要 priced timed automata 或在 zone 上做优化，而不只是 region reachability。

模型常数若是有理数，可统一缩放为整数；若允许任意不可比较实常数，有限区域构造的有效编码前提会改变。

Zone 与 DBM ​

工具常用 zone 表示一组满足差分约束 $x-y\le c$ 的估值，并以 difference-bound matrix 存储。时间后继、guard 交、reset 和 canonical closure 都有矩阵运算。

zone 不等于 region：它通常更粗地一次容纳许多区域，并在探索中按需生成。为保证有限终止，需要 extrapolation 把超过最大常数的界截断；截断必须保持待验证性质。

zone 图节点是 (location, zone)。到达同一位置的两个 zone 若一个包含另一个，可在适当可达性任务中用 inclusion subsumption 合并；删除方向必须与 over-approximation 保证一致，否则会漏行为。

严格不等式、无穷界和整数/实数时间语义会影响 DBM 规范化。把 < 当 <= 会在边界制造或删除行为。

模型边界 ​

标准时间自动机时钟都以同一速率增长，reset 到零，不能暂停或任意赋值。stopwatch automata、hybrid automata 等扩展可使可达性迅速变得不可判定。

Zeno 路径在有限总时间内执行无限多离散步。若现实规格只接受 time-divergent 行为，模型检查必须显式排除 Zeno，不能因每步延迟非负就默认时间趋于无穷。

多个时钟若由同一事件 reset，会产生精确相等关系；zone 能保存 $x-y=0$，逐时钟上下界却会丢掉它。选择 region、zone 或独立区间不只影响性能，也决定后续 guard 能否排除伪路径。

现实系统时钟有漂移和测量误差。理想模型假设同速精确时钟；若结论对微小扰动不鲁棒，应使用 robust semantics 或扩大 guard，而不是把实现偏差归为模型检查器误差。

参考资料

• Rajeev Alur and David Dill, “A Theory of Timed Automata,” Theoretical Computer Science 126(2), 1994, pp. 183–235。
• Johan Bengtsson and Wang Yi, “Timed Automata: Semantics, Algorithms and Tools,” in Lectures on Concurrency and Petri Nets, Springer, 2004, pp. 87–124。
• Gerd Behrmann, Alexandre David, and Kim G. Larsen, “A Tutorial on UPPAAL,” SFM-RT, Springer, 2004, pp. 200–236。