有限状态系统的抽象定义及CEGAR分析解析理论篇

一、有限状态系统的抽象定义及相关阐述

1、有限状态系统定义

有限状态系统（Finite state system, FSS） $T$ 由多个关键部分构成：

• 有限状态集合 $Q$：它代表系统所有可能处于的状态，是一个有限集。例如在简单的自动售货机模型中，状态可能包括 “空闲”“已投币”“商品已售出” 等，每个状态描述了系统在某一时刻的特定条件或配置。
• 转移标签集合 $\Sigma$：这些标签表示能够触发系统状态间转移的符号。在自动售货机的例子里，转移标签可以是 “投币”“选择商品”“出货” 等，它们代表了能使系统从一个状态转变到另一个状态的事件或输入。
• 初始状态 $q_{init}$：属于 $Q$ 集合，是有限状态系统开始运行时所处的状态。对于自动售货机，初始状态可能就是 “空闲” 状态。
• 转移函数 $\to \subseteq Q\times \Sigma \times Q$：此函数定义了系统如何基于输入符号从一个状态转移到另一个状态。若 $(q_1,a,q_2)\in \to$，意味着当系统处于状态 $q_1$ 且接收到输入符号 $a\in \Sigma$ 时，会转移到状态 $q_2$。比如，若 $(“空闲”,“投币”,“已投币”)\in \to$，表明自动售货机在 “空闲” 状态下接收到投币操作后，会转变为 “已投币” 状态。

2、 有限状态系统间的抽象关系（Abstract）

抽象关系的定义，可以基于函数，也可以基于等价关系来定义。

2.1 基于函数的抽象定义

设 $T_1$ 和 $T_2$ 为两个有限状态系统。若存在函数 $\alpha :Q_1\to Q_2$，满足以下两个条件，则称 $T_2$ 是 $T_1$ 的抽象，记为 $T_1\prec T_2$：

• 初始状态对应：$\alpha (q_{init}^1)=q_{init}^2$，即该函数将 $T_1$ 的初始状态 $q_{init}^1$ 映射到 $T_2$ 的初始状态 $q_{init}^2$，确保两个系统的起始点以一致的方式关联。
• 转移对应：对于 $T_1$ 中的每一个转移 $q_1{\stackrel{a}{\to }}_1{q}_2$，在 $T_2$ 中都有对应的转移 $\alpha (q_1){\stackrel{a}{\to }}_2\alpha (q_2)$。这表明 $T_1$ 在输入 $a$ 时的行为，通过函数 $\alpha$ 在 $T_2$ 中得到体现。

例如，设 $T_1$ 为一个较为详细的自动售货机有限状态系统，
其状态集 Q 1 = { q 空闲 , q 1 元币投入 , q 2 元币投入 , q 选择商品 , q 出货 } Q_1 = \{q_{空闲}, q_{1 元币投入}, q_{2 元币投入}, q_{选择商品}, q_{出货}\} Q1​={q空闲​,q1元币投入​,q2元币投入​,q选择商品​,q出货​}，
转移标签集 Σ 1 = { 投 1 元币 , 投 2 元币 , 选择商品 , 出货 } \Sigma_1=\{投 1 元币, 投 2 元币, 选择商品, 出货\} Σ1​={投1元币,投2元币,选择商品,出货}，
初始状态 $q_{init}^1=q_{空闲}$，
转移关系为 $\{(q_{空闲},投1元币,q_{1元币投入}),(q_{空闲},投2元币,q_{2元币投入}),(q_{1元币投入},选择商品,q_{选择商品}),(q_{2元币投入},选择商品,q_{选择商品}),(q_{选择商品},出货,q_{出货})\}$。
设 $T_2$ 为一个简化的自动售货机有限状态系统，
其状态集 Q 2 = { q 未投币 , q 已投币 , q 出货 } Q_2=\{q_{未投币}, q_{已投币}, q_{出货}\} Q2​={q未投币​,q已投币​,q出货​}，
转移标签集 Σ 2 = { 投币 , 选择商品 , 出货 } \Sigma_2 = \{投币, 选择商品, 出货\} Σ2​={投币,选择商品,出货}，
初始状态 $q_{init}^2=q_{未投币}$，
转移关系为 $\{(q_{未投币},投币,q_{已投币}),(q_{已投币},选择商品,q_{出货}),(q_{出货},出货,q_{出货})\}$。

定义函数 $\alpha (q_{空闲})=q_{未投币}$，$\alpha (q_{1元币投入})=\alpha (q_{2元币投入})=q_{已投币}$，$\alpha (q_{选择商品})=\alpha (q_{出货})=q_{出货}$。此时，$\alpha (q_{init}^1)=\alpha (q_{空闲})=q_{未投币}=q_{init}^2$，并且对于 $T_1$ 中的转移，如 $q_{空闲}{\stackrel{投1元币}{\to }}_1{q}_{1元币投入}$，在 $T_2$ 中有 $\alpha (q_{空闲}){\stackrel{投币}{\to }}_2\alpha (q_{1元币投入})$（因为 $\alpha (q_{空闲})=q_{未投币}$ 且 $\alpha (q_{1元币投入})=q_{已投币}$ 且 $q_{未投币}{\stackrel{投币}{\to }}_2{q}_{已投币}$），其他转移也类似满足对应关系，所以 $T_2$ 是 $T_1$ 的抽象（$T_1\prec T_2$）。

2.2 基于等价关系的抽象定义

给定 $T_1$ 状态集 $Q_1$ 上的一个等价关系 $\sim \subseteq Q_1\times Q_1$，可按如下方式定义 $T_1$ 的抽象 $T_2=T_1/\sim$：

• 状态集：$T_2$ 的状态集 $Q_2=Q_1/\sim$，即 $Q_2$ 的元素是 $Q_1$ 在等价关系 $\sim$ 下的等价类。
• 转移关系：在 $T_2$ 中，当且仅当存在 $q_1\in q_2$ 和 $q_1^{\prime }\in q_2^{\prime }$（其中 $q_2$ 和 $q_2^{\prime }$ 是 $Q_2$ 中的等价类），使得在 $T_1$ 中有 $q_1{\stackrel{a}{\to }}_1{q}_1^{\prime }$ 时，才有转移 $q_2{\stackrel{a}{\to }}_2{q}_2^{\prime }$。

继续以自动售货机为例，设 $T_1$ 的状态集 Q 1 = { q 空闲 , q 1 元币投入 , q 2 元币投入 , q 选择商品 , q 出货 , q 找零 } Q_1=\{q_{空闲}, q_{1 元币投入}, q_{2 元币投入}, q_{选择商品}, q_{出货}, q_{找零}\} Q1​={q空闲​,q1元币投入​,q2元币投入​,q选择商品​,q出货​,q找零​}，转移标签集 Σ 1 = { 投 1 元币 , 投 2 元币 , 选择商品 , 出货 , 找零 } \Sigma_1 = \{投 1 元币, 投 2 元币, 选择商品, 出货, 找零\} Σ1​={投1元币,投2元币,选择商品,出货,找零}，转移关系为 $$\{(q_{空闲},投1元币,q_{1元币投入}),(q_{空闲},投2元币,q_{2元币投入}),(q_{1元币投入},选择商品,q_{选择商品}),(q_{2元币投入},选择商品,q_{选择商品}),(q_{选择商品},出货,q_{出货}),(q_{2元币投入},找零,q_{找零})\}$$

定义等价关系 $\sim$ 如下：如果两个状态在货币处理方式上相同，则它们等价。即 $q_{1元币投入}\sim q_{2元币投入}$（因为都涉及投币操作，只是金额不同），$q_{空闲}$ 自成一个等价类，$q_{选择商品}$ 自成一个等价类，$q_{出货}$ 自成一个等价类，$q_{找零}$ 自成一个等价类。

那么 $Q_2=Q_1/\sim =\{[q_{空闲}],[q_{1元币投入}],[q_{选择商品}],[q_{出货}],[q_{找零}]\}$（其中 $[q_{空闲}]$ 是 $q_{空闲}$ 的等价类，$[q_{1元币投入}]$ 是 $q_{1元币投入}$ 和 $q_{2元币投入}$ 的等价类等）。

对于 $T_1$ 中的转移 $q_{1元币投入}{\stackrel{选择商品}{\to }}_1{q}_{选择商品}$，因为 $q_{1元币投入}\in [q_{1元币投入}]$ 且 $q_{选择商品}\in [q_{选择商品}]$，所以在 $T_2=T_1/\sim$ 中有 $[q_{1元币投入}]{\stackrel{选择商品}{\to }}_2[q_{选择商品}]$。同理，对于 $T_1$ 中的其他转移，也可按此规则确定 $T_2$ 中的转移关系。

二、 基于上面的定义出发，提出的思考

1. 为什么我们想要/需要进行抽象

• 答案：为了获得“更简单”的系统
• 解释：在实际应用中，复杂系统的分析和理解往往具有很高的难度。以自动售货机的有限状态系统为例，一个详细描述的自动售货机状态系统可能包含众多状态，如不同货币投入状态、各种商品选择状态、找零状态等，以及复杂的转移关系。这种复杂性使得对系统进行全面分析，例如验证其是否正常工作、是否存在安全漏洞等变得十分困难。通过抽象，我们可以将这些复杂的状态和关系进行简化，去除一些不必要的细节，从而得到一个更易于理解和处理的“更简单”的系统。例如，将不同货币投入状态合并为一个“已投币”状态，这样就减少了状态数量，使得系统结构更加清晰，便于我们进行分析和研究。

2. 抽象是否保留所有属性

• 答案：不。它保留特定的属性。
• 解释：抽象是对原始系统的一种简化表示，它必然会舍弃一些细节。在有限状态系统的抽象过程中，不是所有原始系统的属性都会被保留下来。例如，在自动售货机从详细状态系统到简化状态系统的抽象过程中，详细系统中关于投入不同金额货币的区分这一属性，在简化抽象系统中可能就不再保留。但抽象会保留某些特定属性，这些属性通常是与我们关注的系统关键行为或特性相关的。例如，系统从“未投币”状态经过“投币”操作可以进入“已投币”状态，进而进行“选择商品”和“出货”等基本行为属性会被保留，以确保抽象后的系统仍然能够反映原始系统的核心功能。

3. 示例：如果抽象是安全的，那么原始系统就是安全的

• 解释：这是抽象保留特定属性的一个体现。在系统安全性方面，如果我们对一个系统进行抽象后，发现抽象后的系统满足安全要求，即不存在安全风险，那么可以推断原始系统也是安全的。这是因为抽象过程虽然简化了系统，但保留了与安全性相关的关键特征和行为。例如，在自动售货机系统中，如果抽象后的系统在各种操作流程下都不会出现商品未付款就出货、投币丢失等安全问题，那么由于抽象保留了这些关键行为的逻辑，原始的详细系统同样也不会出现这些安全问题。因为抽象系统是基于原始系统构建的，其安全行为是对原始系统安全相关行为的一种提炼和保留。

4. 抽象总能证明一个安全系统的安全性吗

• 答案：不。可能没有得到合适的抽象。
• 解释：虽然抽象在一定程度上能够反映原始系统的属性，但并不是所有的抽象都能有效地证明原始系统的安全性。如果抽象过程中过度简化，丢失了与安全性紧密相关的关键信息，那么即使抽象后的系统看起来是安全的，也不能确定原始系统一定安全。例如，在自动售货机系统中，如果抽象时将投币验证环节完全简化掉，使得抽象系统中不存在投币验证相关状态和转移，那么这个抽象系统可能看似“安全”（因为没有涉及投币验证相关的错误可能），但实际上原始系统中存在投币验证这一关键安全环节，所以不能依据这个抽象系统来证明原始系统的安全性。这就说明，只有合适的抽象，即保留了与安全性相关的关键属性和行为的抽象，才能用于证明原始安全系统的安全性。

5. 我们如何寻找“合适”的抽象

• 答案：Refinement!（细化！）
• 解释：细化是寻找合适抽象的一种方法。当我们最初得到的抽象可能不理想，没有保留我们所需要的关键属性时，就需要对抽象进行细化。以自动售货机为例，如果最初的抽象系统过于简化，丢失了投币验证环节，我们可以通过细化操作，重新引入与投币验证相关的状态和转移关系，使抽象系统更加接近原始系统的真实行为，从而保留关键属性。通过不断地对抽象进行调整和细化，使其既能简化原始系统以便于分析，又能保留我们关注的关键属性，如安全性、功能性等，最终得到一个“合适”的抽象，能够有效地用于对原始系统的分析和验证。

6. 细化的定义

• “Let T1 be a FSS and T2 its abstraction.
• “A refinement of T2 is an FSS T3 such that T1 ≺ T3 ≺ T2.”
  设T1是一个有限状态系统（FSS），T2是它的抽象。T2的一个细化是一个有限状态系统T3，使得T1 ≺ T3 ≺ T2。这里定义了细化的概念，即存在一个新的有限状态系统T3，它与T1和T2存在特定的抽象关系。T1是原始系统，T2是T1的抽象系统，而T3是对T2的细化，T3比T2更接近T1，在抽象程度上处于T1和T2之间。也就是说，T3相对于T2保留了更多T1的细节和特性，但又不像T1那样复杂，仍然具有一定的抽象性。

7. 如何进行细化的方法

一种方法是——反例引导的抽象细化（CEGAR）。CEGAR（Counter - Example - Guided Abstraction Refinement，反例引导的抽象细化）的方法。CEGAR方法通常基于对抽象系统分析过程中发现的反例，来指导对抽象系统进行细化，使其更精确地反映原始系统的行为，从而在抽象与原始系统之间找到一个更合适的中间系统，即实现对抽象系统的细化。

三、CEGAR分析流程解析

可达性问题设定

首先，我们面临一个可达性问题：给定一个状态 $q_f$，从有限状态系统 $T_1$ 的初始状态出发，能否到达该状态 $q_f$ 呢？这个问题是整个分析流程的核心关注点，我们后续的所有操作都是围绕判断这个可达性展开。

在程序bug查错的问题中，可以将出错分支添加一个可达性检查，如果执行到出错分支，那么就说明程序出错了。

1、 构建抽象系统 （抽象）

为了简化问题的分析，我们构建一个 $T_1$ 的抽象系统 $T_2$。通过抽象，我们将复杂的 $T_1$ 系统简化为一个更容易分析的 $T_2$ 系统，但同时保留了与可达性问题相关的关键特征。

2、 对抽象系统进行模型检查 （检查）

在得到抽象系统 $T_2$ 后，我们对其进行模型检查。具体检查的内容是：从 $T_2$ 的初始状态出发，能否到达状态 $\alpha (q_f)$ 呢？这里的 $\alpha$ 是从 $T_1$ 到 $T_2$ 的抽象映射函数，将 $T_1$ 中的状态 $q_f$ 映射到 $T_2$ 中的 $\alpha (q_f)$。

2.1 模型检查结果判断 - 答案为否，$T_1$ 是安全的

如果模型检查的答案是“否”，即从 $T_2$ 的初始状态无法到达 $\alpha (q_f)$，那么我们可以得出结论：$T_1$ 是安全的。这是因为抽象系统 $T_2$ 虽然简化了 $T_1$，但保留了可达性相关的关键属性。如果在 $T_2$ 中都无法到达对应的抽象状态，那么在更复杂的原始系统 $T_1$ 中也必然无法到达目标状态 $q_f$，所以可以判定 $T_1$ 是安全的。

2.2 模型检查结果判断 - 答案为是，不确定

如果模型检查的答案是“是”，即从 $T_2$ 的初始状态可以到达 $\alpha (q_f)$，此时我们不能直接得出关于 $T_1$ 的确定性结论，只能说“不确定”。因为抽象系统可能因为简化而引入了一些在原始系统中不存在的“虚假”路径。

当答案为“是”时，模型检查会返回一条在 $T_2$ 中到达 $\alpha (q_f)$ 的路径，这条路径被称为“ **抽象反例 **”。它展示了在抽象系统 $T_2$ 中从初始状态到 $\alpha (q_f)$ 的一种可能的执行路径。

3、 验证抽象反例 （验证）

得到抽象反例后，我们需要检查这个抽象反例是否在原始系统 $T_1$ 中有对应的“具体反例”，这个过程称为验证。

3.1 验证结果判断 - 存在具体反例， 不安全

如果经过验证，发现抽象反例在原始系统 $T_1$ 中有对应的具体反例，那么我们就找到了一个真正的反例，这表明原始系统 $T_1$ 是不安全的。因为这个具体反例展示了从 $T_1$ 的初始状态可以到达我们关注的状态 $q_f$，而这个状态可能代表了某种不安全的情况，比如自动售货机在未付款时就出货的状态等。

3.2 验证结果判断 - 不存在具体反例，虚假的

如果验证后发现抽象反例在原始系统 $T_1$ 中没有对应的具体反例，那么这个抽象反例就是“虚假的“spurious””。也就是说，它是由于抽象过程的简化而产生的，在实际的原始系统 $T_1$ 中并不存在这样的执行路径。

4、利用虚假抽象反例进行细化 （细化）

对于虚假的抽象反例，我们利用它来对抽象系统 $T_2$ 进行细化。通过分析虚假抽象反例产生的原因，我们可以在抽象系统中添加更多的细节，使其更接近原始系统 $T_1$ 的真实行为，从而得到一个更精确的抽象系统。例如，如果虚假抽象反例是由于在抽象过程中忽略了某个关键状态或转移关系导致的，我们就可以在细化过程中重新引入这些元素。经过细化后，我们可以再次对新的抽象系统进行模型检查和后续的验证步骤，不断重复这个过程，直到能够确定原始系统 $T_1$ 的可达性情况。

通过这样的 CEGAR 分析流程，我们能够逐步深入地分析复杂的有限状态系统 $T_1$ 的可达性问题，通过抽象、检查、验证和细化等步骤，在简化分析的同时确保分析结果的准确性。

四、关于验证的详细说明

在有限状态系统（FSS）的分析过程中，验证是一个关键环节，用于确定从抽象系统（如 $T_2$）中得到的反例在原始系统（如 $T_1$）中是否真实存在。

1、反例表示

在抽象系统 $T_2$ 中，我们得到一个反例路径：${\sigma }_0=q_0^1\stackrel{a_1}{\to }{q}_0^2\stackrel{a_2}{\to }{q}_0^3\cdots \stackrel{a_k}{\to }{q}_0^{k+1}$，此路径作为 $T_2$ 中的反例。

2、验证的定义

验证的核心问题是：在原始系统 $T_1$ 中是否存在这样一条路径 $\sigma =q_1\stackrel{a_1}{\to }{q}_2\stackrel{a_2}{\to }{q}_3\cdots \stackrel{a_k}{\to }{q}_{k+1}$，满足以下条件：

1. $q_1=q_{init}^1$，即路径起始于 $T_1$ 的初始状态。
2. $q_{k+1}=q_f$，即路径最终到达我们关注的状态 $q_f$。
3. 对于所有的 $i$，都有 $\alpha (q_i)=q_0^i$，这里的 $\alpha$ 是从 $T_1$ 到 $T_2$ 的抽象映射函数，意味着 $T_1$ 路径上的状态通过抽象映射后与 $T_2$ 反例路径上的状态相对应。

3、验证过程

• a. 定义可达状态集合：对于 $1\le i\le k+1$，我们计算 $Reac{h}_i$，它表示所有能够 “模仿”$q_0^i\stackrel{a_i}{\to }\cdots \stackrel{a_k}{\to }{q}_0^{k+1}$ 并最终到$q_f$ 的状态集合。
• b. 初始化 $Reac{h}_{k+1}$：首先，明确 R e a c h k + 1 = { q f } Reach_{k + 1} = \{q_f\} Reachk+1​={qf​}，因为在路径的最后一步，只有目标状态 $q_f$ 能够满足到达 $q_f$ 的条件。
• c. 计算其他 $Reac{h}_i$ 集合：对于 $1\le i\le k$，通过公式 $Reac{h}_i={\alpha }^{-1}(q_0^i)\cap Pre(Reac{h}_{i+1},a_i)$ 来计算$Reac{h}_i$。其中，${\alpha }^{-1}(q_0^i)$ 表示在 $T_1$ 中通过抽象映射 $\alpha$ 能映射到$q_0^i$ 的所有状态集合；$Pre(Reac{h}_{i+1},a_i)$ 表示在 $T_1$ 中通过输入 $a_i$ 能够到达$Reac{h}_{i+1}$ 集合中状态的所有前置状态集合。通过取这两个集合的交集，我们得到$Reac{h}_i$，即满足既能够通过抽象映射对应到 $q_0^i$，又能通过输入 $a_i$ 到达下一步状态集合 $Reac{h}_{i+1}$ 的状态集合。

4、验证结果判定

存在具体的路径 $\sigma$（即原始系统 $T_1$ 中存在与抽象系统 $T_2$ 反例对应的真实反例）当且仅当（iff） $Reac{h}_0\ne \varnothing$。如果 $Reac{h}_0$ 不为空集，说明在 $T_1$ 的初始状态集合中，存在能够按照我们所期望的路径，通过一系列状态转移最终到达 $q_f$ 的状态，也就意味着找到了与抽象反例对应的具体反例；反之，如果 $Reac{h}_0$ 为空集，则表明在 $T_1$ 中不存在这样的路径，即抽象反例是虚假的，在原始系统中并不存在对应的真实反例。

通过以上验证过程，我们能够准确判断抽象系统中的反例在原始系统中是否真实有效，从而进一步对系统的安全性、可达性等性质进行准确分析。

五、基于反例分析的细化过程介绍

在对有限状态系统进行分析时，基于反例分析的细化是优化抽象系统的重要手段。以下详细阐述该细化过程：

1、确定关键索引 $j$

首先，我们通过反向计算来寻找一个关键的整数 $j$。在这个过程中，我们关注计算得到的一系列集合 $Reac{h}_i$。$j$ 被定义为满足 $Reac{h}_j=\varnothing$ 的最大整数，也就是说，在反向计算过程中，$Reac{h}_j$ 是第一个变为空集的集合。这一步骤的关键在于通过分析 $Reach$ 集合序列，找到抽象与原始系统行为出现偏差的关键位置，因为空集的出现暗示了在抽象过程中丢失了某些必要的状态或转移关系，需要进行修正。

2、分析集合关系

在确定了 $j$ 之后，我们考察 $Post({\alpha }^{-1}(q_0^j))$ 和 $Reac{h}_{j+1}$ 这两个集合的关系。这里，${\alpha }^{-1}(q_0^j)$ 表示在原始系统 $T_1$ 中通过抽象映射 $\alpha$ 能映射到抽象系统 $T_2$ 中状态 $q_0^j$ 的所有状态集合，而 $Post({\alpha }^{-1}(q_0^j))$ 则是这些状态通过一次转移后所能到达的状态集合。我们发现 $Post({\alpha }^{-1}(q_0^j))\cap Reac{h}_{j+1}=\varnothing$，这表明从能映射到 $q_0^j$ 的原始状态出发，经过一次转移后到达的状态集合，与后续应该能够到达目标状态 $q_f$ 的状态集合 $Reac{h}_{j+1}$ 没有交集。这种不相交的情况进一步说明了在抽象过程中，状态 $q_0^j$ 的抽象可能过度简化，导致了状态转移的不连续性，需要对其进行调整。

3、构建新的抽象系统 $T_3$

为了修正这种过度简化的情况，我们对状态 $q_0^{j+1}$ 进行拆分。将 $q_0^{j+1}$ 拆分成两个状态，使得其中一个状态包含 $Post({\alpha }^{-1}(q_0^j))$，另一个状态包含 $Reac{h}_{j+1}$。通过这种拆分方式，我们在抽象系统中引入了更多的细节，使得抽象系统能够更好地反映原始系统的状态转移关系。经过这样的处理后，我们就得到了新的抽象系统 $T_3$。这个新的抽象系统 $T_3$ 相较于之前的抽象系统 $T_2$，在保留原始系统关键特性的同时，更准确地模拟了原始系统的行为，从而在后续的分析中能够提供更可靠的结果。

通过以上步骤，基于反例分析的细化过程能够有效地优化抽象系统，使其更符合原始系统的真实情况，为进一步准确分析系统的性质和行为提供了有力支持。

六、参考文献

主要参考：https://mitras.ece.illinois.edu/ECE584/Archives/2012/lectures/Lecture20.pdf