DFA#
一個正規語言(Regular Language)的語法可以用一個正則表達式(Regular Expression)來描述,或者用一個確定有限自動機(Definite Finite Automation,DFA)來表達,例如:
一個僅包含字符 a 和 b,且他們各自出現次數均為偶數的字符串。
可以表示為
其中 q0 既是起始態,也是終結態。
如果將該 DFA 視為一個黑盒,用戶輸入一個字符串之後僅能夠得到該字符串是否符合該文法的布爾值(accept /reject),那麼通過不斷的嘗試符號的組合,並且根據是否符合文法的判斷來反向推斷文法 / DFA,就可以看作是學習狀態模型(state model)的過程。
Definitions, Notations#
一個 DFA 由五元組 表示:
- 是有限的所有可能出現的狀態集合。
- 是有限的所有可能出現的符號集合。
- 是狀態轉移規則:在某個狀態下輸入某個符號,自動機會跳轉到下一個狀態。
- 是終結狀態的集合。
- 是初始狀態。
Observation Table, OT#
L* 算法的核心是一張表 ——Observation Table(OT),一個 OT 可以表示為三元組 $(S_D,E_D,T_D)$:
- 包含前綴封閉的字符串集合,是表格的行索引的一部分。這些字符串表示可能存在的狀態,被稱作 access string。
- 包含後綴封閉的字符串集合,是表格的列索引的集合。這些字符串用於區分不同的狀態(即定義狀態的等價關係),被稱作 distinguish string。OT 中任意取出兩行 $s,t$,若他們對應的每個 distinguish string 的項的取值都相等(也就是說這兩行的內容完全相同),那麼這兩行對應的狀態就是等價的,記作 。等價的狀態可以被歸並為 1 個狀態,在 DFA 中表示為 1 個節點。
- : 表示表中每行每列的項。其中行索引不僅包含 ,還包含 ,後者為每個可能的 後加上一個符號組成的字符串的集合。 的取值由字符串 (直接相連)能否被 accept 決定,是一個布爾值。
- OT 表中真正表示狀態的行為 , 跟多的只是用於輔助判斷狀態之間跳轉關係的。
要使得 OT 能夠表示成一個合理的 DFA,需要滿足兩個性質:
- 封閉性(closed):因為 表示從一個狀態出發,添加一個符號,到達的下一個狀態,這個新的狀態如果與所有 中的狀態都不等價,那就說明存在至少一個新狀態,即 OT 不封閉,還可以繼續拓展。將來在構造 DFA 時,就知道每一個狀態 添加任意一個符號 之後會跳轉到的目的狀態,如果目的狀態已經存在在 中了,那無妨,但如果不存在在 $S_D$ 中,那就說明還有新的狀態沒有探索到。
- 一致性(consistent):對於任意兩個等價的狀態 ,對於每一個符號 ,都要有 。如果不成立,那就說明 s、t 不是等價的,因為從他們出發通過同一個符號可能會到達不同的狀態。等價關係根據當前 OT 的列索引(distinguish string)產生,因此在列索引產生變化之後等價關係同樣也會發生變化。一般而言,對於一個狀態的認識是從模糊到精確的過程,所以先前被認為是等價的關係往往隨著 distinguish string 的增加會變為不等。
L* Algorithm#
- 初始化 ,並且連同 一道構造 OT 的所有行。
- 為了獲得每一行的項的取值,向 oracle 進行 membership query:對於 ,詢問 oracle 從狀態 s 出發經過符號 e 的路徑是否能夠 accept。填充整張表。
- 判斷是否為封閉和一致:
- 如果不封閉,就從 中取出一個不封閉的行,移動到 部分。
- 如果不一致,即 ,就將 加入到 distinguish string 中。橫向拓展 OT,並通過 membership query 填充表內內容。
- 如果一致,通過 OT 構造 DFA,向 oracle 提出 equivalence query(等價查詢):
- 如果不等價,oracle 會返回 counter example(反例),將反例的所有前綴 string 添加到 中,並拓展 ,回到步驟二。
- 如果等價,那麼就結束了。
Example#
Reverse Engineering Enhanced State Models of Black Box Software Components to support Integration Testing 給出的例子的完整過程如下。假設 oracle 有如下的 DFA。
其 , 為 加上 中的每個符號(),初始狀態 。
- 該 OT 既是一致的,但不封閉,因為 在 中沒有與其等價的行(),因此把 (即 )移入 中。
- 由於 a 被新添加到了 ,所以 需要添加 ,對 oracle 做 membership query,得到 。
- 此時 OT 是封閉且一致的,且只有 2 個等價類,一類是 ,另一類是 ,這兩個等價類反映到圖上就是 2 個狀態,並且結合後一個類上添加字符 a 和 b 到達的不同的狀態,可以得到 DFA。
- 此時做等價查詢,得到反例 沒有被構造出的 DFA 滿足。將 的所有前綴()添加到 OT 的 中,並且將 加入到 。
- 此時 OT 是否封閉的,但不一致,因為等價狀態 添加同一個符號 後的 ,說明 實際上並不等價,需要做進一步區分,區分的依據即為狀態 再添加一個符號 之後可能跳轉的狀態。
- 添加了 之後,對 oracle 做 membership query,填滿整個 OT,上一個 OT 中等價的 a、b 此時也已經不等價了。
- 此時 OT 是一致且封閉的,可以構造成 DFA。
- 對 oracle 做 equivalence query,得到反例 雖然是構造出的 DFA 所能 accept,但是 oracle 對其 reject。將 的所有前綴加入 (這裡只需要再添加 即可),並且向 添加 。
- 此時 OT 是封閉但不一致的,因為 ,則需要把 也加入 ,橫向拓展 OT。
- 對 oracle DFA 做 membership query,填充整張表,此時表式封閉且一致的,構造出的 DFA 與 oracle DFA 經過 equivalence query 判別也是等價的。
- 最終就得到了 oracle DFA 的結構。
Conclusion#
- OT 表分為上下兩個部分,上半部分 用字符串(符號串)來表示,下半部分 則是用於輔助判斷 的跳轉目標是否已知,若已知的話應對應於某個 ,若未知則說明 中還應有新的成員。
- L* 算法學習的過程本質上是對各個狀態的認識從模糊到逐步清晰的過程。
- 當 OT 不封閉時,說明需要添加新狀態了,視野進一步擴大。
- 當 OT 不一致時,說明對於等價狀態的認識需要進一步細化了。
- 是區分不同狀態的特徵值,在 DFA 中,兩個狀態的等價可以理解為:這兩個狀態分別經過相同的符號都能夠跳轉到終結態,或者都不能夠跳轉到終結態。
參考資料: