布奇自动机(Büchi automata)

\(\omega\)-自动机
设\(\Sigma\)是一个有限的字母表。定义在字母表\(\Sigma\)上的自动机\[A = (Q, \Sigma, \delta, Q_0,Acc)\]称为\(\omega\)-自动机，其中Q是一个有限的状态集合，\(\delta:Q\times \Sigma\to Q\)是一个状态转移函数，\(Q_0\)为初始状态，\(Acc\)为接受条件，形式化定义为\(Q^\omega\)的子集，这里\(Q^\omega\)表示由Q中元素构成的全体无穷序列。

\(\omega\)-自动机和有穷自动机的区别在于其关注无穷状态序列的计算，而有穷自动机研究最终停机的有限计算。但是\(\omega\)自动机并非真正运行一个无穷序列的计算，而是提供了一种将无穷计算表示为有限结构的方式，来研究它的性质。我们接下来研究的布奇自动机是一种特殊的\(\omega\)-自动机。

布奇自动机(Büchi automata)
一个布奇自动机定义为\[A = \langle \Sigma, S, \Delta, I , L ,F\rangle,\]这里\(\Sigma\)是一个有限的字母表，\(S\)是有限的状态集合，\(\Delta\subseteq S\times S\)是状态转换关系，\(I\subseteq\)是初始状态集，\(L:S\to\Sigma\)是状态上的标签集，\(F\subseteq S\)是接受状态集。注意，我们这里定义的布奇自动机是非确定性(nondeterministic)的\(\omega\)-自动机，而上面的定义是指确定性的\(\omega\)-自动机。
对于A的一次计算\(\rho\), 定义\(inf(\rho)\)为其状态序列中出现了无穷多次的状态的集合。在布奇自动机中，我们定义A接受\(\rho\)当且仅当\[\inf(\rho)\cap F\ne \emptyset.\]也就是说，运算\(\rho\)中至少有一个状态s出现了无穷多次，并且s在接受状态集F中。对于非确定性布奇自动机，如果给定一个输入，只要有一种可行的计算被接受，这个输入就被认为是可接受的。
最后，我们用\(L(A)\subseteq \Sigma^\omega\)表示布奇自动机A接受的语言。注意，这里的字母表\(\Sigma\)是在状态上贴的性质标签。

利用自动机验证的一大优势是系统的模型和它的性质用一种同样的方式表示。我们将一个系统表示为布奇自动机\(A = \langle 2^{AP}, S, \Delta, I , L ,F\rangle\), 这里AP是命题标签的幂集，\(L:S\to 2^{AP}\)是标签函数。
一般情况下，我们定义S中所有状态都是可接受状态。而在需要检验程序的公平性(fairness)时，我们会选取一些状态作为可接受状态。

确定性布奇自动机
确定性与非确定性布奇自动机并非等价的。例如，不存在一个确定性布奇自动机，使其字母表为\(\{A,\lnot A\},\)并且使得接受计算当且仅当A至多出现有限次，但可以构造一个(非确定性的)布奇自动机实现这一点。另外，确定性布奇自动机在补运算下也不封闭。

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