写给学生看的系统分析与验证笔记（十一）—

写给学生看的系统分析与验证笔记（十一）——Generalized NBA(GNBA)

本文主要是介绍写给学生看的系统分析与验证笔记（十一）——Generalized NBA(GNBA)，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

Generalized NBA

GNBA也是由一个五元组 $\mathcal{G}=(Q,Σ,q_{0},\mathcal{F},δ)$ 构成，其中 $Q,Σ,q_{0}.δ$ 含义都与NBA中的一样，但是F表示为接受状态集合的集合(set of accept sets)，表示为 $\mathcal{F}\subseteq 2^Q$ ， $\mathcal{F}$ 可以是类似 ${F_{1},F_{2},...,F_{k}\}$ 的形式。

对GNBA来说，如果一个运行 $q_{0}q_{1}q_{2}...$ 是可接受的，那么表示，每个接受状态集合将会被无限经常次访问。

直白说，NBA的F是一个集合，它要求运行可以无限经常次访问接受状态集合里面的元素，而GBNA的 $\mathcal{F}$ 是一个集合的集合，它要求运行可以无限经常次访问集合里面的每一个集合中的元素，这么看来GNBA的确是一种广义的NBA，当GNBA的F中只有一个集合的时候，就变成了NBA。

用符号表示为：
$\forall F∈\mathcal{F}\text{ }\overset{∞}\exist\text{ }i∈N s.t. q_{i}∈F$

GNBA可接受的语言表示为：
$L_{\omega}(\mathcal{G})=\{\sigma∈Σ^\omega|无限字\sigma输入自动机存在一条可接受的运行\}$

用GNBA表示活性(liveness)
在这里插入图片描述
两个进程无限经常次进入临界区，这个LT属性可以用GNBA表示，此时的 $\mathcal{F}=\{\{q_{1}\},\{q_{2}\}\}$

GNBA转NBA

首先我们要知道，对于每一个GNBA来说，存在一个NBA使得
$L_{\omega}(\mathcal{G})=L_{\omega}(\mathcal{A})$

$\mathcal{F}=\{F_{1},F_{2},...,F_{k}\}$ ，当k＝1时，它就是一个NBA，而当k＞1时
在这里插入图片描述
从初始状态 $Q_{0}$ 出发，我们可以将 ${F_{1},F_{2},...,F_{k}\}$ 分成k个GNBA的拷贝，要注意的是，只有在某个拷贝中访问了接受集合 $F_{k}$ 后才能访问下一个拷贝，这样依次下去，直到几个拷贝连成环，这样就生成了一个NBA

接下里讲述具体的算法：

假设 $\mathcal{G}=(Q,Σ,Q_{0},\mathcal{F},δ)$ 是一个GNBA， $A=(Q',Σ,Q'_{0},F',δ')$ 是一个NBA，为了顺利转换，我们需要在状态上增添常数i，用它表示某个状态属于第i个部分

$Q'=Q×\{1,2,...k\}$
$Q'_{0}=Q_{0}×\{1\}=\{<q_{0},1> |q_{0}∈Q_{0}\}$
$F'_{1}=F_{1}×\{1\}=\{<q_{0},1> |q_{F}∈F_{1}\}$
$δ'(<q,i>,a)=\begin{cases}\{q'.i\}|q'∈δ(q,a)\text{ }if\text{ }q\notin F_{i}\\ \{q'.i+1\}|q'∈δ(q,a)\text{ }otherwise \end{cases}$

大致公式就如上面所示， $Q_{0}$ 和 $F_{1}$ 都标记为第一个部分，发生转换时，如果当前状态不属于 $F_{i}$ ，则下一个状态的标记i不变，如果当前是 $F_{i}$ 中的状态发生了转换，那么下一个标记需要加1（其实这个公式还少了一部分，如果处于最后一个标记的的F，那么下一个标记应该仍未1）