自动机验证(Automatic Verification)

利用自动机验证的框架
我们即将展示的模型展示方法是基于自动机理论(automata theory)的。这允许我们将待验系统和形式化规范以相同的方法表出，即布奇自动机。
假设我们希望系统模型A满足形式规范B。于是我们只需要证明自动机接受的语言满足\[L(A)\subseteq L(B).\]这等价于\[L(A)\cap \overline{L(B)}=\emptyset.\]如果交集非空，我们就得到了A不满足B的一个反例。
事实上，验证两个自动机语言交集为空要比验证其包含关系容易得多。不过，生成一个自动机语言的补集是比较困难的。然而，如果我们采用线性时序逻辑(LTL)，我们可以避免考虑补集，只需要将\(\varphi\)改为\(\lnot\varphi\)即可。

布奇自动机的结合
我们将构造性地证明布奇自动机的语言在交集和闭集运算下是封闭的。
考虑两个有共同字母表的自动机\(A_1 = \langle \Sigma, S_1, \Delta_1, I_1,L_1, F_1\rangle,\) 和\(A_2 = \langle \Sigma, S_2, \Delta_2, I_2,L_2,F_2\rangle.\)

构造\(A_1\cup A_2\)是容易的。我们不妨假定\(S_1\cap S_2 = \emptyset\)，否则重新命名状态即可。定义
\[A_1 \cup A_2 = \langle \Sigma, S_1 \cup S_2, \Delta_1 \cup \Delta_2 ,I_1\cup I_2 , L_1\cup L_2, F_1 \cup F_2 \rangle,\]于是\(L(A_1\cup A_2) = L(A_1)\cup L(A_2).\) 事实上，自动机在开始时有一个非确定性的选择，既可以选择根据\(A_1\)运行，也可以选择根据\(A_2\)运行，这由对初始状态的选择决定。

下面我们考虑\(A_1\cap A_2\). 其接受的语言应当同时被\(A_1, A_2\)接受，因此当\(A_1\cap A_2\)运行时，应当模拟\(A_1, A_2\)同时运行。所以我们即将构造的状态集似乎是\(S_1\times S_2\). 但是这样的构造会给接受状态集的构造造成麻烦，我们将无法定义合适的接受状态集\(F\subseteq S_1\times S_2\).

于是我们还需要定义一种特殊的自动机：广义布奇自动机(generalized Büchi automaton).
广义布奇自动机的变化之处在于其接受状态集\(F=\{f_1,\cdots, f_m\}, f_i\subseteq S\)，使得一次计算\(\rho\)被接受当且仅当 \(\forall i,inf(\rho) \cap f_i\ne \emptyset\), 换言之每个\(f_i\)都有至少一个状态在该计算序列中出现了无穷多次。

我们接下来定义广义布奇自动机\(A_1\cap A_2.\) 其状态集\(S = S_1\times S_2\), 转移函数\(\Delta \), 初始状态集\(I_1\times I_2\), 标签函数\(L\), 接受状态集\(\{F_1\times S_2, S_1\times F_2\}\).
转移函数要求同时模拟\(A_1, A_2.\) 因此\[(\langle s_1, s_2\rangle , \langle s'_1,s'_2\rangle)\in \Delta \Leftrightarrow (s_1,s'_1)\in \Delta_1\land (s_2,s'_2)\in \Delta_2.\]注意标签函数是将状态集映射为命题变量集，因此\(L(s_1, s_2)=L_1(s_1)\land L_2(s_2),\) 即两个命题的合取。如果合取后的命题可化简为false，应当删去这个状态。
注意接受状态集既要求模拟计算中的\(A_1\)经过无穷多次\(F_1\)中的某元素，也要求\(A_2\)经过无穷多次\(F_2\)中的某元素，因此这个定义是合适的。

最后，我们指出如何从广义布奇自动机转化为布奇自动机，以完成\(A_1\cap A_2\)的构造。
设广义布奇自动机的接受状态集F有m个元素（即m个S的子集），我们如下定义(平凡)布奇自动机：
状态集\(S' = \bigcup_{i=1}^m S_i,\) 这里\(S_i = S\times \{i\}.\)每个状态具有形式\((s,i),s\in S.\)
状态转移关系\(\Delta'\)，\((\langle s , i\rangle ,\langle s' ,j\rangle)\in \Delta'\)当且仅当以下之一成立：
(1) \(s\in f_i,\ j=i+1\)（下标按模m理解）;
(2) \(s\not\in f_i,\ j=i\).
这意味着，当且仅当s在\(f_i\)中时，i才能切换到i+1. 于是，一个计算能够无穷多次经过某一组\(f_i\times i\)，当且仅当其无穷多次经过了每一组\(f_i\times i\).
由此，初始状态集\(I\times\{1\},\) 标签集\(L':L'(s,i)=L(s)\), 接受状态集\(F'=f_1\times\{1\}\)的定义是自然的。

到目前为止，我们证明了布奇自动机在交和并运算下是封闭的。除此之外，还可以证明布奇自动机在补运算下也是封闭的，在此不再赘述。

布奇自动机语言的非空性检验
如上所述，欲证明自动机A满足形式规范B，只需验证\(L(A)\cap\overline{L(B)}=\emptyset\)，即只需检验某个自动机语言是否非空。我们继续做如下观察：
将自动机A的状态及其转移关系视为一个有向图。对任意一个A的计算\(\rho\)，一定存在某个后缀\(\rho'\)，使得\(\rho'\)的任意一个状态都在之后出现了无穷多次。（因为A的状态集是有限的，出现了有限次的状态一定在\(\rho\)中总共出现了有限次，将这一段前缀删去后即得到\(\rho'\).）
于是，\(\rho'\)中的状态形成了一个强连通分支，它们恰好就是\(inf(\rho)\)。另一方面，从初始状态出发的、可达的任一个强连通分支，也生成了自动机的一个运算。因此，检验\(L(A)\)的非空性又转化成了寻找A的可达的强连通分支。

将线性时序逻辑LTL转化成自动机
下面我们给出一种算法，将线性时序逻辑LTL的一个形式规范\(\varphi\)转化成等价的布奇自动机。
自动机的每个节点(node) s与一个公式(formula) \(\eta(s)\)相关联，满足：对任一个可接受计算\(\xi\), 如果此计算达到了状态s，设其后缀是\(\xi^i\)，那么我们将得到\(\xi^i\vDash \eta(s)\).
公式\(\eta(s)\)将具有如下形式：\[(\bigwedge_{i=1...m} \nu_i)\land\bigcirc (\bigwedge_{j=1...n}\kappa_j).\]这是为了方便生成节点的后继节点。每个LTL公式可以令\(m=1,n=0\)来直接转化成此形式。
我们的想法是化简上述形式的公式。首先，我们注意到\[\mu\bigcup\psi \equiv \psi\lor(\mu\land\bigcirc \mu\bigcup\psi).\]于是我们可以将\(\mu\bigcup\psi\)指向两个子节点，都删去这个公式，其一在\(\mu_i\)中添加\(\psi\)，另一个在\(\nu_i\)中添加\(\mu\)，并且在\(\kappa_j\)中添加\(\mu\bigcup\psi\).
用这个方法同样可以处理\(\mu\bigvee\psi, \mu\land\psi,\mu\lor\psi,\bigcirc\mu.\) 于是，我们可以逐步消去所有的\(\bigcup,\bigvee,\land,\lor,\bigcirc.\)
现在还差\(\lnot,\Diamond,\Box\)没有解决。对于后两者，只需要注意到\(\Diamond\psi\equiv true\bigcup \psi\)和\(\Box\psi\equiv false\bigvee\psi.\) 而对于\(\lnot\)，我们采用"向内递归"(inwards)将所有公式化为"规范否定形式"(negation normal form)，即满足所有\(\lnot\)符号只能写在命题变量之前，如\(\lnot(\mu\lor\eta)\equiv (\lnot\mu)\land(\lnot\eta).\) 类似不难给出其余公式的递归方法。

至此我们可以化简所有的公式。用形式化的语言来描述，一个节点(node)包括以下内容：
(1) 名称(Name)，节点的唯一标识。
(2) 入口(Incoming)，一列指向此节点的节点。
(3) 新公式(New)，旧公式(Old)和下一公式(Next). 每一部分都是一个子公式集。
每个节点代表了某些计算的后继\(\xi^k\)的时序性质(Temporal properties). 公式\(New(s)\cup Old(s)\)即以上的\(\nu_i\)，其中\(Old(s)\)代表了那些已经处理过的公式。而\(Next(s)\)即以上的\(\kappa_j\).

设我们想要转化的LTL公式是\(\varphi\)。转换开始时，先构造一个初始节点，仅包括\(\varphi\)一个公式在New中，并且有唯一的入口init。init可以视为一个特殊的节点。
我们如下递归地构造节点图。
对于当前节点s(从init开始构造)，检查New(s)是否有未处理的公式。
(1) 若否，则此节点的处理已完成。于是再去检查节点集中是否存在另一个节点r，使得这两个节点的Old和Next分别完全相同。此时，我们不再需要节点s，将指向s的节点转而指向r，并删去s。如果不存在这样的r，则我们将s添加到节点集中，我们获得了新的"当前节点" s'，满足：
[1] s指向s'
[2] New(s')=Next(s)
[3] Old(s'), Next(s')被初始化为空集。
(2) 若是，任选New(s)中一个公式\(\eta\)，将其从New中删去并移入old中，选择\(\eta\)的一个主运算符，按照以上给出的处理公式的方法，获得一至两个新节点。将New(s), Old(s), Next(s), Incoming(s)全都赋给新节点。注意，经此操作后New(s)减少。经过有限次类似操作后，New(s)将变为空集。当节点图构造完成时，所有节点的New均为空。

经过有限步操作后，公式\(\varphi\)对应的有向图构造已经完成。最后，我们再构造与\(\varphi\)等价的(广义)布奇自动机：\[B=\langle \Sigma, S, \Delta, I,L,F\rangle.\]字母表\(\Sigma\)包括AP的命题及其否定形式组成的公式；状态集S即为图中的各个节点；\(\Delta\)是图的有向边；初始状态集I是由init指向的节点组成；L(s)是Old(s)中的公式的合取；接受条件F是一些AP的子集f组成的集合族，每个元素f对应一种\(\mu\bigcup\psi\)，使得f中的节点s满足：要么\(\psi\in Old(s)\)，要么\(\mu\bigcup\psi\not\in Old(s).\)

模型检验的复杂性
如何度量模型检验的输入对决定模型检验的复杂性有很大影响。从时间角度来看，布奇自动机的检验可以在P时间内（甚至NL空间内）完成，但以LTL表示的模型检验是PSPACE空间的。事实上，LTL验证无论是相对于待验系统还是待验公式，都是PSPACE完全的。但从空间的角度来看，LTL形式的验证，只需要与其等价的布奇自动机指数小的空间。在实践中，我们需要相对简短、容易理解、应用广泛的验证形式。
因此，我们一般选取LTL作为验证的形式规范。

状态爆炸(State Space Explosion)问题的应对策略
如何减轻状态爆炸问题成为了模型检验的主要挑战。以下我们列举了几种可能有效的策略。
(1) 二元决策图(Binary Decision Diagrams, BDD)
二元决策图是用来表达一个布尔函数的数据结构。利用二元决策图可以避免分别地计算并存储每一个状态，而是将所有状态存储在一个不含圈的图表(DAG)中。
(2) 偏序简化(Partial Order Reduction)
偏序简化用于缩减状态空间的大小，只需要检验一部分计算即可。它充分利用了并发系统中转换的可交换性。
(3) 对称性(Symmetry)
这种方法是基于利用状态组成部分的置换(permutation). 在某些特定的置换下，一些状态之间将没有区别。因此只需要选取一些状态的代表进行检验即可。

    所属分类：Formal Methods     发表于2022-02-04