什么是符号模型检验
模型检验就是检验一个模型是否具有我们想要的特征。我们在遇到实践问题的时候，首先应该对问题进行数学或逻辑建模，然后通过“运算”看看模型是否有矛盾或者模型是否具有正常的功能。通常情况下，一个小的模型凭借肉眼心算就可以找出错误。但是在模型有成百上千个节点的时候，单靠人是绝无可能分析的。所以就需要借助数学的力量。符号模型检验是基于有限自动机（FSM，或叫做有限状态机），引入OBDD技术解决状态量爆炸的技术。
有限自动机
有限自动机
M
=
(
Q
,
Σ
,
δ
,
q
0
,
F
)
M=(Q,\Sigma,\delta,q_0,F)
M=(Q,Σ,δ,q0,F)由5个部分组成，分别是
一个有限状态集合
Q
=
{
q
0
,
q
1
,
…
…
q
n
}
Q=\{q_0,q_1,……q_n\}
Q={q0,q1,……qn} ，用来描述系统中的不同状态。在任何一个确定的时刻，系统只会处在唯一一个状态中。
一个输入符号集合
Σ
=
{
σ
0
,
σ
1
,
…
…
σ
m
}
\Sigma=\{\sigma_0,\sigma_1,……\sigma_m\}
Σ={σ0,σ1,……σm}，用来表征系统所接受的不同输入信号。在任何一个确定的时刻，系统只能受到一个确定的信号。
一个状态转移函数
δ
:
Q
×
Σ
→
Q
\delta: Q\times\Sigma\to Q
δ:Q×Σ→Q，用来描述系统在接受不同输入时从一个状态转到另一个状态的规则。如在某一刻系统处在状态
q
i
q_i
qi，接受到信号
σ
j
\sigma_j
σj，那么下一时刻将处在状态
q
′
=
δ
(
q
i
,
σ
j
)
q'=\delta(q_i,\sigma_j)
q′=δ(qi,σj)。
规定
q
=
δ
(
q
,
ε
)
q=\delta(q,\varepsilon)
q=δ(q,ε)，即输入空信号（没有信号）时不发生状态转移。
定义
δ
(
q
,
a
b
)
=
δ
(
δ
(
q
,
a
)
,
b
)
,
a
,
b
∈
Σ
\delta(q,ab)=\delta(\delta(q,a),b),a,b\in\Sigma
δ(q,ab)=δ(δ(q,a),b),a,b∈Σ，即可以输入字符串,相当于按顺序读取。
初始状态
q
0
∈
Q
q_0\in Q
q0∈Q，终止状态集
F
⊆
Q
F\subseteq Q
F⊆Q
在现在的问题之下，我们更关注于
Q
,
Σ
,
δ
Q,\Sigma,\delta
Q,Σ,δ，所以也用三元组
M
=
(
Q
,
Σ
,
δ
)
M=(Q,\Sigma,\delta)
M=(Q,Σ,δ)表示。
状态转移函数可以用三种方式来表示：状态转移图，状态转移表，状态转移矩阵。
先来看一个例子
模3计数器
在这个例子中有状态
Q
=
{
0
,
1
,
2
}
Q=\{0,1,2\}
Q={0,1,2}，初始状态为
q
0
=
0
q_0=0
q0=0
有输入
Σ
=
{
i
n
c
,
d
e
c
}
\Sigma=\{inc,dec\}
Σ={inc,dec}
i
n
c
inc
inc：加1；
d
e
c
dec
dec：减1；
我们可以得出以下关系
δ
(
0
,
i
n
c
)
=
1
,
δ
(
1
,
i
n
c
)
=
2
,
δ
(
2
,
i
n
c
)
=
0
\delta(0,inc)=1,\delta(1,inc)=2,\delta(2,inc)=0
δ(0,inc)=1,δ(1,inc)=2,δ(2,inc)=0
δ
(
0
,
d
e
c
)
=
2
,
δ
(
1
,
d
e
c
)
=
0
,
δ
(
2
,
d
e
c
)
=
1
\delta(0,dec)=2,\delta(1,dec)=0,\delta(2,dec)=1
δ(0,dec)=2,δ(1,dec)=0,δ(2,dec)=1
其状态转移图为
状态转移表为
| 状态 | 输入inc | 输入dec |
|---|---|---|
| 0 | 1 | 2 |
| 1 | 2 | 0 |
| 2 | 0 | 1 |
状态转移矩阵为
0
1
2
0
1
2
(
i
n
c
d
e
c
d
e
c
i
n
c
i
n
c
d
e
c
)
\begin{matrix} 0 \quad& 1 &\quad 2 \end{matrix} \\ \begin{matrix} 0 \\ 1 \\2 \end{matrix}\begin{pmatrix} & inc & dec \\ dec & &inc \\ inc&dec& \end{pmatrix}
012012⎝⎛decincincdecdecinc⎠⎞
有限自动机还不足以描述现实的有限状态系统。现实情况下输入数据除了希望内部状态改变外，还希望向外部输出信号，从而引出两类推广。moore机就是输出与状态有关的系统，mealy机是输出与状态和输入都有关的系统。
Moore机
moore机是有限自动机的推广。
Moore机
M
=
(
Q
,
Σ
,
Δ
,
δ
,
λ
,
q
0
)
M=(Q,\Sigma,\Delta,\delta,\lambda,q_0)
M=(Q,Σ,Δ,δ,λ,q0)的定义为
一个有限状态集合
Q
=
{
q
0
,
q
1
,
…
…
q
n
}
Q=\{q_0,q_1,……q_n\}
Q={q0,q1,……qn}
一个输入符号集合
Σ
=
{
σ
0
,
σ
1
,
…
…
σ
m
}
\Sigma=\{\sigma_0,\sigma_1,……\sigma_m\}
Σ={σ0,σ1,……σm}
一个输出符号集合
Δ
=
{
a
0
,
a
1
,
…
…
a
r
}
\Delta=\{a_0,a_1,……a_r\}
Δ={a0,a1,……ar}
一个状态转移函数
δ
:
Q
×
Σ
→
Q
\delta: Q\times\Sigma\to Q
δ:Q×Σ→Q
一个输出函数
λ
:
Q
→
Δ
\lambda: Q \to \Delta
λ:Q→Δ
初始状态
q
0
∈
Q
q_0\in Q
q0∈Q
moore机没有包含终止状态部分。并且在每个状态都有输出。
例如对于输入串
σ
0
σ
1
…
σ
k
\sigma_0\sigma_1…\sigma_k
σ0σ1…σk,若有函数
δ
(
q
0
,
σ
0
)
=
q
1
\delta(q_0,\sigma_0)=q_1
δ(q0,σ0)=q1
δ
(
q
1
,
σ
1
)
=
q
2
\delta(q_1,\sigma_1)=q_2
δ(q1,σ1)=q2
……
δ
(
q
k
,
σ
k
)
=
q
k
+
1
\delta(q_{k},\sigma_k)=q_{k+1}
δ(qk,σk)=qk+1
则输出为
λ
(
q
0
)
λ
(
q
1
)
…
λ
(
q
k
+
1
)
\lambda(q_0)\lambda(q_1)…\lambda(q_{k+1})
λ(q0)λ(q1)…λ(qk+1)
看一个例子
二进制模3余数器
在这个例子中有状态
Q
=
{
q
0
,
q
1
,
q
2
}
Q=\{q_0,q_1,q_2\}
Q={q0,q1,q2}分别代表此刻的余数，初始状态为
q
0
q_0
q0
有输入
Σ
=
{
0
,
1
}
\Sigma=\{0,1\}
Σ={0,1}，输出
Δ
=
{
0
,
1
,
2
}
\Delta=\{0,1,2\}
Δ={0,1,2},输出函数
λ
(
q
i
)
=
i
,
i
=
1
,
2
,
3
\lambda(q_i)=i,i=1,2,3
λ(qi)=i,i=1,2,3
状态转移图为
当输入串10100时输出为012212
输
入
状
态
输
出
ε
q
0
0
1
q
0
q
1
01
10
q
0
q
1
q
2
012
101
q
0
q
1
q
2
q
2
0122
1010
q
0
q
1
q
2
q
2
q
1
01221
10100
q
0
q
1
q
2
q
2
q
1
q
2
012212
\begin{array}{|c|c|c|} 输入 & 状态 & 输出 \\ \hline \varepsilon&q_0&0\\ 1&q_0q_1&01\\ 10&q_0q_1q_2&012\\ 101&q_0q_1q_2q_2&0122\\1010&q_0q_1q_2q_2q_1&01221\\10100&q_0q_1q_2q_2q_1q_2&012212\\ \end{array}
输入ε110101101010100状态q0q0q1q0q1q2q0q1q2q2q0q1q2q2q1q0q1q2q2q1q2输出001012012201221012212
Mealy机
Mealy机
M
=
(
Q
,
Σ
,
Δ
,
δ
,
λ
,
q
0
)
M=(Q,\Sigma,\Delta,\delta,\lambda,q_0)
M=(Q,Σ,Δ,δ,λ,q0)的定义为
一个有限状态集合
Q
=
{
q
0
,
q
1
,
…
…
q
n
}
Q=\{q_0,q_1,……q_n\}
Q={q0,q1,……qn}
一个输入符号集合
Σ
=
{
σ
0
,
σ
1
,
…
…
σ
m
}
\Sigma=\{\sigma_0,\sigma_1,……\sigma_m\}
Σ={σ0,σ1,……σm}
一个输出符号集合
Δ
=
{
a
0
,
a
1
,
…
…
a
r
}
\Delta=\{a_0,a_1,……a_r\}
Δ={a0,a1,……ar}
一个状态转移函数
δ
:
Q
×
Σ
→
Q
\delta: Q\times\Sigma\to Q
δ:Q×Σ→Q
一个输出函数
λ
:
Q
×
Σ
→
Δ
\lambda: Q\times\Sigma\to \Delta
λ:Q×Σ→Δ
初始状态
q
0
∈
Q
q_0\in Q
q0∈Q
mealy机与moore机不同的是输入不仅依赖状态，而且依赖输入。当输入串长为n时，输出长为n，而不是n+1。
给出以下一个例子
用a/b标记表示输入/输出
q
0
q_0
q0表示初始状态，
q
1
q_1
q1表示输入的末尾字符为0，
q
2
q_2
q2表示输入的末尾字符为1。
输出
{
y
，
n
}
\{y，n\}
{y，n}表示接受或拒绝此字符串。
对于输入串01100,输出为nnyny。
具有条件和变量机制的有限状态机
有限自动机可以携带条件和变量。
看下面例子
此系统为简单的身份认证系统，密码为ABA，最大允许错误为三次，err为报警状态，c为计数变量。
X[con]/Y[exec]表示输入为X且条件con成立下，转移至下一状态，然后输入Y且执行exec。
有限状态机的复合
系统通常是由多个模块组成的。需要对各个模块的有限自动机进行复合，复合的最简单方式是笛卡尔积。
对于有限状态机
M
1
=
(
Q
1
,
Σ
1
,
δ
1
,
q
10
)
M_1=(Q_1,\Sigma_1,\delta_1,q_{10})
M1=(Q1,Σ1,δ1,q10),
M
2
=
(
Q
2
,
Σ
2
,
δ
2
,
q
20
)
M_2=(Q_2,\Sigma_2,\delta_2,q_{20})
M2=(Q2,Σ2,δ2,q20)的笛卡尔积为
M
=
M
1
×
M
2
=
(
Q
,
Σ
,
δ
,
q
0
)
M=M_1\times M_2=(Q,\Sigma,\delta,q_0)
M=M1×M2=(Q,Σ,δ,q0)
其中
Q
=
Q
1
×
Q
2
Q=Q_1\times Q_2
Q=Q1×Q2
Σ
=
(
Σ
1
∪
{
ε
}
)
×
(
Σ
2
∪
{
ε
}
)
\Sigma=(\Sigma_1 \cup\{\varepsilon\}) \times (\Sigma_2 \cup\{\varepsilon\})
Σ=(Σ1∪{ε})×(Σ2∪{ε})
q
0
=
(
q
10
,
q
20
)
∈
Q
q_0=(q_{10},q_{20})\in Q
q0=(q10,q20)∈Q
δ
(
(
q
1
,
q
2
)
,
(
σ
1
,
σ
2
)
)
=
\delta((q_1,q_2),(\sigma_1,\sigma_2))=
δ((q1,q2),(σ1,σ2))=
{
(
q
1
′
,
q
2
)
δ
1
(
q
1
,
σ
1
)
=
q
1
′
,
σ
1
∈
Σ
1
,
σ
2
=
ε
(
q
1
,
q
2
′
)
δ
2
(
q
2
,
σ
2
)
=
q
2
′
,
σ
1
=
ε
,
σ
2
∈
Σ
2
(
q
1
′
,
q
2
′
)
δ
1
(
q
1
,
σ
1
)
=
q
1
′
,
δ
2
(
q
2
,
σ
2
)
=
q
2
′
,
σ
1
∈
Σ
1
,
σ
2
∈
Σ
2
无
定
义
其
余
\begin{cases} (q_1',q_2) & \delta_1(q_1,\sigma_1)=q_1',\sigma_1\in\Sigma_1 ,\sigma_2= \varepsilon \\ (q_1,q_2') &\delta_2(q_2,\sigma_2)=q_2',\sigma_1= \varepsilon,\sigma_2\in\Sigma_2 \\ (q_1',q_2') & \delta_1(q_1,\sigma_1)=q_1',\delta_2(q_2,\sigma_2)=q_2',\sigma_1\in\Sigma_1,\sigma_2\in\Sigma_2 \\无定义 &其余 \end{cases}
⎩⎪⎪⎪⎨⎪⎪⎪⎧(q1′,q2)(q1,q2′)(q1′,q2′)无定义δ1(q1,σ1)=q1′,σ1∈Σ1,σ2=εδ2(q2,σ2)=q2′,σ1=ε,σ2∈Σ2δ1(q1,σ1)=q1′,δ2(q2,σ2)=q2′,σ1∈Σ1,σ2∈Σ2其余
给出一个例子
模3计数器和模4计数器的复合
模3计数器和模4计数器状态转移图为
复合模型具有3*4=12种状态。而输入有3*3=9种，考虑到 ( ε , ε ) (\varepsilon,\varepsilon) (ε,ε)不发生转移，每个状态都会有8种状态转移。一共12*8=96种状态转移。