正则性质

有限自动机
一个未定有限自动机(Nondeterministic Finite Automaton, NFA)是指五元组\[A=\langle Q,\Sigma, \delta,Q_0, D\rangle,\] 其中Q是有限的状态集合,\(\Sigma\)是字母表,\(\delta: Q\times \Sigma \to 2^Q\)是迁移函数,\(Q_0\)是初始状态集合,\(F\subset Q\)为接受状态集。
A接受某个有限单词w,当且仅当存在A的一个运行,使A可以将w读完,且停机在接受状态。A接受单词的集合称为A接受的语言,记作\(L(A)\).

未定有限自动机与确定有限自动机(Deterministic Finit Automation, DFA)是等价的。确定有限自动机是指\(|Q_0|\le 1\)且\(\forall q, A, |\delta(q, A)|\le 1|.\) 这一结论由迁移函数扩充到Q的幂集上可以立即得到。如果\(|Q_0|=1, |\delta(q,A)|=1,\) 称DFA是完全的。通过添加陷阱状态及其自循环可以证明DFA与完全DFA的等价性。

有限自动机的非空性与可达性是等价的,即\(L(A)\ne\emptyset \Leftrightarrow \exists q_0\in Q,q\in F\), 使得\(q\in Reach(q_0).\)

利用构造同步积等方法,可以证明有限自动机的语言(即正则语言)在交、并、补、连接和有限次重复(Kleene*)下是封闭的。

正则安全性质的模型检验
定义 正则安全性质:若\(P_{safe}\)的坏前缀集合构成字母表\(2^{AP}\)上的正则语言,称为正则安全性质。
不变式都是正则安全性质,坏前缀可由\(\Phi^*(\lnot \Phi) true^*\)刻画,这里\(\Phi\)表示所有\(A\vDash \Phi, A\in 2^{AP}\)的集合。

为了检验有限迁移系统TS是否满足正则安全性质\(P_{safe}\),只需要构造TS与A的同步积\(TS\otimes A\),其中A是检验正则安全性质的有限自动机,然后检验此迁移系统。利用A的接受状态诱导的命题逻辑公式, 可以得到一个不变式\(\Phi\), 使得\(Traces_{fin}(TS)\cap L(A) = \emptyset\)当且仅当\(TS\otimes A\vDash \Phi.\) 这样,正则安全性质的检验就转化成了不变式的检验。

设TS是无终止状态的迁移系统,\(A=\langle Q, \Sigma, \delta, Q_0, F\rangle\)是NFA,其中字母表\(\Sigma = 2^{AP}\)且\(Q_0\cap F = \emptyset\).定义乘积迁移系统如下:\[TS\otimes A = \langle S', Act, \to ', I', AP', L' \rangle\] 其中\(S' = S\times Q\), \(\rightarrow'\)由以下定义:\[\frac{s\to^a t\land q\overset{L(t)}{\to}p}{\langle s, q\rangle \to^a \langle t, p \rangle}\]\(I'=\{\langle s_0, q\rangle | s_0\in I, \exists q\in Q_0:q_0\overset{L(s_0)}{\to}q\}\),
\(AP'=Q\), \(L':S\times Q\to 2^Q\)由\(L'(\langle s, q\rangle)=\{q\}\)给出,AP'的不变式\(P_{inv(A)}\)由命题公式\[\bigwedge_{q\in F} \lnot q\]定义,简记为\(\lnot F\).

定理:TS是AP上的迁移系统,A是字母表为\(2^{AP}\)的NFA,\(P\)是AP上的正则安全性质,\(L(A)\)是其(极小)坏前缀的集合。以下命题等价:
(1) \(TS\vDash P\).
(2) \(Traces_{fin}(TS)\cap L(A)=\emptyset\).
(3) \(TS\otimes A \vDash P_{inv}(A)\).

无限单词上的自动机
\(\omega\)正则表达式:形如\[G = E_1\cdot F_1^\omega + \cdots+E_n\cdot F_n^\omega\]其中\(E_i, F_i\)为字母表\(\Sigma\)上的正则表达式,且\(\epsilon \not \in L(F_i)\). \(F^\omega\)表示无限次重复,与有限次重复\(F^*\)对应。\(\omega\)正则语言关于交、并、补是封闭的。

若AP上的LT性质P是字母表\(\Sigma = 2^{AP}\)上的正则语言,则称P是\(\omega\)正则性质。
不变式、无饥饿是\(\omega\)正则性质。无饥饿可由正则表达式\[((\{\}+\{wait\})^*\cdot (\{crit\}+\{wait, crit\}))^\omega\]描述。

未定布奇自动机(Nondeterministic Büchi Automata, NBA)是指五元组\[A=(Q, \Sigma, \delta, Q_0, F)\] 其中\(\delta: Q\times \Sigma \to 2^{Q}\)是迁移函数,\(F\subseteq Q\)是接受状态集。更多布奇自动机相关的内容可以参考布奇自动机自动机验证, 如确定布奇自动机DBA和广义未定布奇自动机GNBA。

定理1. NBA接受的语言类和\(\omega\)正则语言的类相等。
定理2. 每个GNBA都存在NBA使二者接受语言类相等。
推论3. GNBA接受的语言类与\(\omega\)正则语言的类相等。
定理4. GNBA接受的语言类在交运算下封闭。
推论5. \(\omega\)正则语言在交运算下封闭。

模型检验\(\omega\)正则性质
类似正则安全性质与NFA同步积的验证,我们利用布奇自动机来检验\(\omega\)正则性质。
设TS是无终止状态的迁移系统,A是无阻塞NBA,定义迁移系统\(TS\otimes A\):与NFA验证正则安全性质的同步积类似,不同之处在于要验证的性质由不变式\(P_{inv(A)}\)变为持久性质\(P_{pers(A)}\):"终将总是\(\lnot F\)."

定理:TS是AP上、无终止状态的有限迁移系统,A是字母表为\(2^{AP}\)的无阻塞NBA,\(P\)是AP上的\(\omega\)正则性质,\(L_\omega(A) = (2^{AP})^\omega -P\)。以下命题等价:
(1) \(TS\vDash P\).
(2) \(Traces(TS)\cap L_\omega(A)=\emptyset\).
(3) \(TS\otimes A \vDash P_{pers}(A)\).

确定好迁移系统TS后,下一个问题是如何确定\(TS\not\vDash P_{pers}\)成立。事实上,只需要检测是否存在TS的一个环路,使得环路上面有一个可达的、且违反性质的状态s。如果不存在则性质成立,否则我们将得到一个反例。

    所属分类:Formal Methods     发表于2022-02-11