对《Principles of Model Checking》一书时间自动机部分的翻译。

（不全）

时间自动机

到目前为止，我们遇到的逻辑是在描述转移系统（Transition System）如何从一种状态演变到另一种状态的转换系统上进行解释的。但是，没有涵盖时间方面。也就是说，既没有给出状态的停留时间，也没有给出在特定时间间隔内进行转换的可能性的指示。然而，诸如设备驱动程序、咖啡机、通信协议和自动取款机等反应式系统（reactive system）必须及时做出反应——它们是时间关键（Time-critical）的。时间关键的系统的行为通常受到相当严格的时序约束。对于火车交叉口，必须在检测到火车接近时，在一定时间内关闭闸门，以便在火车到达交叉口之前停止汽车和行人的通行。对于放射机来说，癌症患者接受高剂量放射的时间段极为重要；这段时间的小幅延长是危险的，可能会导致患者死亡。

简而言之：

时间关键的系统的正确性不仅取决于计算的逻辑结果，还取决于结果产生的时间

由于对于反应式系统来说，及时性是至关重要的，因此必须保证满足系统的时间约束。检查时间约束是否满足是这一章节的主题。为了表达这样的时间限制，策略将被扩展到允许表达时间顺序的逻辑形式（logical formalisms），以及定量时间的概念。这些扩展允许时间约束表达，如：

“交通灯将在接下来的30秒内变绿“

首先要做的选择是时域（time domain）：它是离散的还是连续的？ 离散时域在概念上很简单。 转移系统用于对时间系统（timed system）进行建模，其中假设每个动作持续一个时间单位。更一般的延时可以用一个专用的不可观察的动作，$\tau$（对于每个tick），来建模。动作$\alpha$持续$k>1$时间单位的事实可以用$k-1$个跟着$\alpha$的（或$\alpha$之前的）滴答动作来建模。这个经典的方法导致了非常大的转移系统。请注意，在此类模型中，任何一对动作的最小时间差都是提前固定的时间单位的倍数。对于同步系统（synchronous），比如，其中涉及的过程以锁步（lockstep）的方式进行，离散时间领域是合适的：一个时间单位对应一个时钟脉冲。在这种情况下，可以使用传统的时间逻辑表达时序约束。下一步操作可以被用来“”度量“过去时间的描述，即，$\bigcirc \Phi$表示了$\Phi$在确切的一个时间单位后满足。通过定义$\bigcirc^{k+1}\Phi=\bigcirc^k(\bigcirc\Phi)$和$\bigcirc^0\Phi=\Phi$,通常的时间约束可以被指定，通过简写$\diamondsuit^{\leq k}\Phi=\bigcirc^0\Phi \vee \bigcirc \Phi \vee \dots \vee \bigcirc^k\Phi$，上述对交通灯的非形式化的时间状态描述可以表示为：

$$\Box(red \Rightarrow \diamondsuit^{\leq 30}green) \nonumber$$

对于同步系统，可以使用 LTL 或 CTL 等转移系统和逻辑来表达时序约束，传统的模型检测算法可以使用。

在这本书中，我们不想将自己限制在同步系统中，而是将像在牛顿物理学中一样考虑具有连续性的时间。 也就是说，非负实数（集合$\mathbb{R}_{\geq0}$ ）将被用作时域。 一个主要优点是不需要预先确定最小时间单位，因为连续时间模型对时间尺度的变化是不变的。 这对于异步系统更合适，例如分布式系统，其中组件可能以不同的速度运行，并且比离散时间模型更直观。 没有附加时序信息的异步系统的转换系统表示确实太抽象了，无法充分模拟时序约束，如下面的示例所示。

示例 9.1. 一个铁路交叉口

考虑一个铁路交叉路口，正如示例2.30（50页）一样，如示意图9.1所示。对于这个铁路示意图，需要开发一个控制系统，在收到一个火车靠近的信号时关闭闸门，收到火车完全通过道路时打开闸门。控制系统应该成立的安全性质是当火车穿过道路时，闸门应该总是关闭的。完整的系统组成包括三个组件：火车、闸门和控制器。

火车 || 闸门 || 控制器

回想一下，一对进程共有的动作需要联合（jointly）执行，而其他动作则是自主（autonomously）执行的。这些进程的转移系统表示如图9.2所示。它遵循组合系统（composite system） 火车||闸门||控制器 不能保证当火车通过交叉口时闸门是关闭的。这可以通过检查组合转移系统的一个初始片段轻松的看到；观察图9.3——在发出“”靠近“信号之后，火车是在闸门关闭前到达道路还是之后到达道路，都无法从转移系统中推断出来。

然而，再假设火车不会超过某个确定的最大速度的情况下，一个信号“接近”和火车已经到达十字路口的时刻之间的时间段的下界，是可以指示的，如图9.4所示。假定火车在发出“接近”信号后，需要至少2分钟到达路口。据此，对控制器和闸门进行了时序假定。在获得“到达”信号是，1分钟后，控制器将会通知放下闸门，闸门确切的关闭时间被家丁不超过1分钟。全局状态中的分支$$可以用时序信息来标注：

火车在超过两分钟之后仅仅可以执行状态迁移$near\xrightarrow{enter} in$。另一方面，闸门在收到“接近”信号之后最多两分钟被关闭。因此，全局状态迁移

$$<near,1,up> \xrightarrow{enter}<in,1,up> \nonumber$$

永不会出现。因此，闸门在火车到达交叉路口前总是关闭的。只要火车在交叉路口，闸门就保持关闭状态的事实通过动作raise仅仅会在火车指示exit后发生的事实得到确认。

根据时间关键系统的形式化建模，时间自动机的概念已经得到发展，这是一种具有测量时间流逝的时钟变量的转移系统（事实上是一个程序图（program graphs））的扩展。这个模型包括对状态和动作的的停留时间施加约束的方法。

9.1 时间自动机

时间自动机对时间关键系统的行为进行建模。时间自动机实际上是一个程序图，它配备了一组有限的实值时钟变量，简称为时钟。时钟不同于通常的变量，因为它们的访问是有限的：时钟只能被查看，以及重置为零。时钟可以重置为零，然后随着时间的推移，它们开始隐式增加它们的值。所有时钟都以速率 1 运行，即在 d 个时间单位过去后，所有时钟都前进 d。因此，时钟的值表示自上次重置以来已经过去的时间量。时钟可以直观地被视为秒表，可以相互独立地启动和查看。时钟值的条件用作动作的使能条件（即$guard$）：只有满足条件才能使能并能够采取动作；否则，该操作将被禁用。依赖于时钟值的条件称为时钟约束。为简单起见，假设启用条件仅取决于时钟而不取决于其他数据变量。 时钟约束还用于限制可能在某个位置花费的时间。 以下定义规定了如何定义时钟约束。

定义 9.2：时钟约束

根据语法形成对时钟集合 $C$ 的时钟约束 ：

$$g::= x<c\ |\ x\leq c\ |\ x>c\ |\ x\geq c\ |\ g \land g \nonumber$$

其中，$c\in \mathbb{N}$且$x\in C$。令$CC(C)$表示$C$上的时钟约束集合。

不包含任何连词的时钟约束是原子性的。 让$ ACC(C)$ 表示 $C $上所有原子时钟约束的集合

时钟约束通常以缩写形式书写，例如，$(x\geq c_1)∧ (x<c_2) $可以缩写为$ x \in [c_1, c_2) $或 $c_1 \leq x<c_2$。 可以以稍微复杂一点的理论为代价添加时钟差约束，例如$ x−y<c$。 为简单起见，这里省略了它们，我们将讨论限制在原子钟约束上，将时钟与常数$ c \in \mathbb{N} $进行比较。如果允许 c 为有理数，则模型检查问题的可判定性不受影响。 在这种情况下，每个公式中的有理数都可以通过适当的缩放转换为自然数。 一般来说，我们可以将每个常数乘以出现在所有时钟约束中的所有常数的最小公倍数。

直观地说，时间自动机是一个（稍作修改的）程序图，其变量是时钟。 时钟用于制定系统行为的实时假设。 时间自动机中的边用$guard$（何时允许选取该边？）、动作（选取该边时执行什么？）和一组时钟（要重置哪些时钟？）来标记。一个位置（location）配备了一个不变量，用于限制可能在该位置花费的时间。 正式定义是：

定义9.3： 时间自动机

一个时间自动机是一个八元组$TA = (Loc,Act,C,\hookrightarrow,Loc_0,Inv,AP,L)$，其中

• $Loc$是位置(location)的有限集合
• $Loc_0 \subseteq Loc$是初始位置的集合
• $Act$是动作的有限集合
• $C$是时钟的有限集合
• $\hookrightarrow \subseteq Loc \times CC(C) \times Act \times2^C\times Loc$是转移关系的集合
• $Inv:Loc\rightarrow CC(C)$是一个不变的赋值函数
• $AP$是一个原子属性的有限集合
• $L:Loc\rightarrow2^{AP}$是对位置(location)的标签函数

$ACC(TA)$表示了发生在$TA$的$guard$或者位置不变量中的原子时钟约束

时间自动机是具有有限时钟集$C$的程序图。边用元组 $(g,\alpha, D)$ 标记，其中$g$是对时间自动机时钟的时钟约束，$\alpha$是一个动作，而$D \subseteq C$ 是一组时钟。$\ell \xhookrightarrow{g:\alpha,D}\ell’$的直观解释是时间自动机可以在时钟约束$g$满足的的情况下从一个位置$\ell$移动到另一个位置$\ell’$。此外，当从位置$\ell$移动到$\ell’$时，$D$中的所有时钟都将重置为零并执行动作$\alpha$。函数$Inv$为每个位置分配一个位置不变量，指定时间自动机可以在那里停留多长时间。对于位置$\ell$ ，$Inv(\ell)$限制了可能在$\ell$中花费的时间量。也就是说，位置应该在不变的$Inv(\ell)$失效之前停留。如果这是不可能的——因为没有启用传出转移——就不可能有进一步的进展。在定义9.11中的时间自动机的形式语义中，这种情况可能导致时间进程停止。由于时间进度不再可能，这种情况也称为死锁。 稍后将更详细地讨论这种现象。 函数$L$具有与转换系统相同的作用，并将在该位置有效的原子命题集与任何位置相关联。

在考虑对时间自动机的精确解释之前，我们先举几个简单的例子

为了描绘时间自动机，我们采用如下的程序图的绘制约定。 不变量在位置内标识，当它们等于真时被省略。 边标有$guard$、动作和要重置的时钟集。 空时钟集经常被省略。 这同样适用于始终为真的时钟约束。 时钟组$D$的复位有时由$reset(D)$ 表示。 如果动作不相关，则省略它们

实例9.4 $Guards$和位置不变量

图 9.5(a) 描绘了一个简单的时间自动机，它有一个时钟$x$和一个配备自环的位置$\ell$。 如果时钟$x$ 值最少到达2，则可以采用自循环，并且在采用时，时钟$x$被重置。 最初，默认时钟$x$的值为 0。

图 9.5(b) 通过描述时钟$x$的值与自从自动机启动以来经过的时间，给出了这个时间自动机的执行示例。 每次时钟重置为 0 时，自动机都会遍历位置$\ell$处的自循环。 由于$Inv(\ell) = true$，居于$\ell$中的时间可以不受任何限制地前进。 尤其是这个自动机的合法行为是将无限期地停留在位置$\ell$上。形式化地，

$$Loc=Loc_0=\{\ell\},C=\{x\},\ell \xhookrightarrow{true:x\geq2,{x}}\ell, 且Inv(\ell)=true \nonumber$$

标签和动作被省略。

通过在位置$\ell$中加入位置不变性$x\leq 3$, 稍微改变图 9.5(a) 的时间自动机，会导致$x$不再无边界的前进的效果。 相反，如果$x\geq 2$ ($guard$) 和$x\leq 3$ (不变式)，则必须进行传出转移。 请注意，没有指定在区间$[2, 3]$ 中的哪个时刻进行转换，即，这是不确定的。 时间自动机及其行为示例分别如图 9.5(c) 和 (d) 所示。

观察到在将图 9.5(a) 中的$guard$加强为$2\leq x\leq 3$ 的同时保持$Inv(\ell) = true$ 时不会获得相同的效果。 在这种情况下，传出转换只能在$2\leq x\leq 3$ 时进行（如前一场景中），但不是强制采用的，即，可以通过在停留$\ell$期间让时间流逝而简单地忽略它。 这在图 9.5(e) 和 (f) 中进行了说明。

简而言之，不变量是强制转换的唯一方法 。

实例 9.5 闸门的时间自动机

考虑铁路道口的闸门（见例 9.1）。 假设降低闸门最多需要一个时间单位，升门需要至少一个和最多两个时间单位，过程Gate的时间自动机如图 9.6 所示。我们有$Act={lowder,raise}$和

$$Loc = \{up,comingdown,down,goingup\} \nonumber$$

且$Loc_0={up}$。时间自动机的转移为：

$$up \xhookrightarrow{true:lower,\{x\}}comingdown \ \ \ comingdwon \xhookrightarrow{true:\tau,\varnothing} down \\ down \xhookrightarrow{true:raise,\{x\}} goingup \ \ \ goingup \xhookrightarrow{x\geq 1:\tau,\varnothing} up \nonumber$$

带有不变式$x\leq 1$的位置$coming\ down$已被添加到模型中，该模型在动作$lower$发生和位置$down$改变之间的最大延迟至多是单个时间单位。 时钟$x$在动作$lower$发生时设置为零，从而“测量”自该事件发生以来的时间流逝。 通过将$coming\ down$的停留时间限制为$x\leq 1$，必须在一个时间单位内切换到$down$。 请注意，这不会通过在带有$guard$ $x\leq1$ 的位置$up$和$down$之间建立直接的边来建立，因为$x$的值不会指代$lower$的发生时间 。以类似的方式，具有不变式$x\leq2$ 的位置$going\ up$的目的是模拟打开阀门最多需要两个时间单位。 在初始位置$up$处，对停留时间没有限制，即$Inv(up) = true$。 这同样适用于位置$down$。 令$AP = {up, down}$，标记函数 $L(up) = { up }，L(down) ={ down }，L(comingdown) = L(goingup) = \varnothing$。

备注 9.6 位置图(Location Diagram)

时间自动机的每个有限行为都可以用位置图表示。 这描绘了直到某个先验固定上限的每个时刻，时间自动机在该行为期间的位置。 对于阀门的定时自动机，一个可能的实时行为由图 9.7 中的位置图指示。

时间自动机的并行组合

对于复杂系统的建模，允许并行组合定时自动机很方便。这允许建模以组合方式对时间关键系统进行分析。 我们考虑一个并行组合算子，记为$||_H$ ，它用一组handshanking动作$H$参数化。这个算子在精神上类似于转换系统上的相应算子； 参见定义 2.26:$H$中的动作需要由两个相关的时间自动机共同执行，而$H$之外的动作则以交错方式自主执行。

时间自动机的握手

假设$TAi = (Loc_i,Act_i,C_i,\hookrightarrow_i,Loc{0,i},Inv_i,AP_i,L_i),i=1,2$是一个时间自动机，$H\subseteq Act_1 \cap Act_2，C_1 \cap C_2=\emptyset,且AP_1 \cap AP_2 = \emptyset$。时间自动机$TA_1 |_H TA_2$可被定义为：

$$(Loc_1 \times Loc_2,Act_1 \cup Act_2,C_1 \cup C_2,\hookrightarrow,Loc_{0,1}\times Loc_{0,2},Inv,AP_1\cup AP_2,L)$$

其中$L(<\ell_1,\ell_2>) = L_1(\ell_1)\cup L_2(\ell_2)$且$Inv(<\ell_1,\ell_2>)=Inv_1(\ell_1)\and Inv_2(\ell_2)$。 转移关系

文章目录

1. 时间自动机
   1. 9.1 时间自动机
      1. 定义 9.2：时钟约束
      2. 定义9.3： 时间自动机
      3. 实例9.4 $Guards$和位置不变量
      4. 实例 9.5 闸门的时间自动机
         1. 备注 9.6 位置图(Location Diagram)
      5. 时间自动机的并行组合
      6. 时间自动机的握手

原文链接: https://zijian.wang/2021/10/19/时间自动机/

版权声明: 转载请注明出处.