时间自动机 | Codeboy's Blog

形式陈述

控制位置与时钟估值

时间自动机由有限位置集合 $L$ 、有限时钟集合 $X$ 、有限边集、位置不变量和指定初始位置 $\ell_0\in L$ 组成。本页取初始估值 $v_0(x)=0$ （对所有 $x\in X$ ），并要求 $v_0\models Inv(\ell_0)$ ；可达性始终从 $(\ell_0,v_0)$ 出发。时钟估值是函数

v:X\to\mathbb R_{\ge0},

使用非负实数记录自上次 reset 后经过的时间。状态是 $(\ell,v)$ ，控制位置有限，估值空间却不可数无限。

边写作

\ell\xrightarrow{a,g,R}\ell',

其中 $a$ 是动作，本页主模型的 guard $g$ 与位置不变量是单时钟约束 $x\bowtie c$ 的有限合取，其中 $c$ 是非负有理常数， $\bowtie\in\{<,\le,=,\ge,>\}$ ， $R\subseteq X$ 是触发后重置为零的时钟集。

它扩展有限状态自动机的离散控制，但不是给每条边附一个固定耗时；时间可以在位置中连续流逝。

两类转移

delay 转移

(\ell,v)\xrightarrow d(\ell,v+d),\qquad d\ge0

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

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

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

直觉

超时协议轨迹

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

一条正常轨迹是

(idle,0)\xrightarrow{request}(waiting,0) \xrightarrow{2.4}(waiting,2.4) \xrightarrow{reply}(done,2.4).

若 waiting invariant 设为 $x\le3$ ，在 $x=3$ 便不能继续正时间延迟；超时 guard $x>3$ 又始终无法在该位置满足。不过响应边 $x\le3$ 在边界仍使能，因此不能无条件声称“没有动作可走”。若响应必须与环境同步而环境不提供响应，系统才可能被困在边界；单看这张自动机，则响应边仍提供离开路径。若设计要求边界即可超时，应把超时 guard 改为 $x\ge3$ 。guard 与 invariant 的开闭端点必须协同。

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

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

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

例子与边界

区域等价

先统一缩放有理常数为整数，设最大常数为 $M$ 。经典区域抽象记录：对 $v(x)\le M$ 的时钟保存实际整数部分 $\lfloor v(x)\rfloor$ ，否则只记“超过 $M$ ”；对未超过 $M$ 的时钟，还保存小数部分是否为零及这些小数部分的相对次序。只保存“有没有超过 $M$ ”不够，例如 $0.2$ 与 $1.2$ 可被 $x\ge1$ 区分。

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

若扩展允许 guard $x-y\bowtie c$ ，就不能原样使用这份区域等价。取 $M=1$ ，估值 $(x,y)=(2,2)$ 与 $(3,2)$ 的两个时钟都超过 $M$ ，会被上述记录合并，但 $x-y\le0$ 在前者为真、后者为假。对角约束仍可用扩展的有限抽象处理，须另行细分区域或证明合适的 zone 模拟关系。

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

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 规范化。把 < 当 <= 会在边界制造或删除行为。

差分约束抽象域与 DBM给出矩阵方向、最短路闭包和一个完整整数循环证书，可作为关系运算的入口。但该页使用整数非严格界，允许把 $i<n$ 写成 $i-n\le-1$ ；这里的实数时钟不能这样转换，还需处理严格界、统一时间流逝、reset 与用于终止的 extrapolation。

模型边界

标准时间自动机时钟都以同一速率增长，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。

形式陈述 ​

控制位置与时钟估值 ​

两类转移 ​

超时协议轨迹 ​

区域等价 ​

Zone 与 DBM ​