定时自动机验证中隐式表示的利用

### 定时自动机验证中隐式表示的利用 在定时自动机验证领域，利用隐式表示可以有效解决状态空间爆炸问题，提升验证效率。下面我们将详细探讨相关内容。 #### 1. 示例过渡描述 首先来看一些示例过渡描述，以惯性参考单元（IRU）的操作为例： ```plaintext ;; The action of switching on an Inertial Reference Unit (IRU). ACTION start_IRU1_warm_up PRECONDITIONS: ’((IRU1 off)) POSTCONDITIONS: ’((IRU1 warming)) DELAY: <= 1 ;; The process of the IRU warming. RELIABLE-TEMPORAL warm_up_IRU1 PRECONDITIONS: ’((IRU1 warming)) POSTCONDITIONS: ’((IRU1 on)) DELAY: [45 90] ;; Sometimes the IRUs break without warning. EVENT IRU1_fails PRECONDITIONS: ’((IRU1 on)) POSTCONDITIONS: ’((IRU1 broken)) ;; If the engine is burning while the active IRU breaks, ;; we have a limited amount of time to fix the problem before ;; the spacecraft will go too far out of control. TEMPORAL fail_if_burn_with_broken_IRU1 PRECONDITIONS: ’((engine on)(active_IRU IRU1) (IRU1 broken)) POSTCONDITIONS: ’((failure T)) DELAY: >= 5 ``` 这些描述展示了IRU从开启预热到正常运行，再到可能出现故障的过程，以及在特定条件下可能导致的失败情况。 #### 2. 隐式表示的优势 在许多问题中，状态空间的大部分子空间是不可达的，这可能是由于控制机制或一致性约束导致的。使用隐式表示结合构造性搜索算法，我们可以避免枚举整个状态空间。以设备预热这样的单个过渡为例，它可以跨越多个离散状态，过渡中心的表示方式能方便地表示这种跨越多个状态的过程。而通过多个自动机相乘来实现类似的表示便利性时，展开乘积构造会导致状态爆炸。 #### 3. CSM算法 给定上述问题表示，控制器综合（规划）问题可以看作是为系统的每个可达离散状态选择一个控制动作。CIRCA的控制器综合问题比一般的定时自动机控制器综合问题更简单，其控制器是无记忆的且不能引用时钟，这有两个优点：一是使综合问题更简单，二是确保生成的控制器在实时系统（RTS）中可实现。 CSM算法的核心是生成安全的控制器，关键在于使失败状态不可达，这通过“抢占”过程实现。一个过渡t在状态s中被抢占，当且仅当从s出发的其他某个过渡t′必须在t可能发生之前发生。CSM通过选择足够快的控制动作来确保在要被抢占的过渡发生之前执行。 其具体步骤如下： 1. 从可达状态集中选择一个状态（在控制器综合开始时，只有初始状态可达）。 2. 对于此状态中启用的每个不可控过渡，选择是否抢占它。导致失败状态的过渡必须被抢占。 3. 为此状态选择一个控制动作或不执行任何操作。 4. 调用验证器确认（部分）控制器是安全的。 5. 如果控制器不安全，使用验证器的信息进行回溯。 6. 如果控制器安全，重新计算可达状态集。 7. 如果没有未规划的可达状态（即所有可达状态都已选择了控制动作），则成功终止。 8. 如果仍有未规划的可达状态，循环到步骤1。 在搜索算法执行过程中，CSM在每次分配控制动作后都会使用验证器。此时，验证器被用作保守启发式方法，将所有未规划状态视为“安全避风港”，进入这些状态的验证轨迹被视为成功。当控制器综合过程完成时，该过程会收敛到一个合理且完整的验证。当验证器表明控制器不安全时，CSM会查询到特定失败状态的路径，路径上的状态集提供了待修订的候选决策。 与博弈论综合控制器设计相比，CSM算法从初始状态开始向前搜索，而博弈论算法通常从不安全状态开始使用不动点操作来寻找可控子空间。此外，CSM算法充分利用了隐式状态空间表示，在许多问题中能够在不访问状态空间大部分区域的情况下找到控制器。 另外，搜索并非盲目进行，使用了基于AI规划开发的与领域无关的启发式方法来指导搜索。同时，还开发了一种分治法的替代搜索方法，在许多问题中能显著提高速度。 #### 4. 验证建模 CSM算法完全在定时问题的离散域中操作，确保控制器易于自动实现。但需要进行路径相关的计算来确定过渡在路径上应用于两个或多个状态时剩余的延迟时间。CSM使用定时自动机验证系统来确保构建的控制器是安全的。 ##### 4.1 执行语义 CIRCA RTS的控制器计算能力有限，这使得控制器综合计算高效，也便于构建提供定时保证的RTS。CSM生成的控制器被编译成一组测试 - 动作对（TAPs）由RTS运行。每个TAP有一个布尔测试表达式，用于区分是否执行特定动作，且这些测试表达式无法访问时钟。例如，用于土星轨道插入领域的一个TAP示例如下： ```plaintext #<TAP 2> Tests: (AND (IRU1 BROKEN) (OR (AND (ACTIVE_IRU NONE) (IRU2 ON)) (AND (ACTIVE_IRU IRU1) (ENGINE ON)))) Acts : select_IRU2 ``` 构成控制器的TAPs被组装成一个循环并进行调度以满足所有TAP的截止日期，截止日期根据控制动作必须抢占的过渡延迟计算得出。 ##### 4.2 定时自动机 定时自动机A是一个元组 \(\langle S, s_i, X, L, E, I \rangle\)，其中： - \(S\) 是有限的位置集。 - \(s_i\) 是初始位置。 - \(X\) 是有限的时钟集。 - \(L\) 是有限的标签集。 - \(E\) 是有限的边集。 - \(I\) 是不变量集。 每条边 \(e \in E\) 是一个元组 \((s, L, \psi, \rho, s')\)，其中 \(s\) 是源位置，\(s'\) 是目标位置，\(L \subseteq L\) 是标签，\(\psi \in \Psi_X\) 是保护条件，\(\rho \subseteq X\) 是时钟重置。在模型中，所有时钟约束形式为 \(c_i \leq k\) 或 \(c_i > k\)，保护条件决定模型何时可以沿着边移动，不变量指示模型何时必须离开状态。定时自动机的状态是一个对 \(\langle s, C \rangle\)，其中 \(s \in S\) 是位置，\(C : X \to Q_{\geq 0}\) 是时钟估值。 当处理复杂系统时，将其视为多个简单自动机的乘积可以简化表示，标签 \(L\) 用于在创建乘积时同步不同自动机的边。 ##### 4.3 用定时自动机建模CIRCA 通过一组相互作用的定时自动机来给出CSM模型的语义。以CIRCA计划图为翻译起点，计划图 \(P = \langle S, E, \overrightarrow{F}, \overrightarrow{V}, \varphi, I, T, \iota, \eta, p, \pi \rangle\