對自動機模型學習問題的分析與研究

張圣迪

摘要：形式化方法在模型為導向的軟件工程中起到非常重要的作用，其中模型檢驗已經成為軟件驗證和糾錯的一種重要方法，而模型學習是對于模型檢驗的一種有效補充技術。本文將對模型學習的概念和研究意義進行介紹，匯總了幾種常見的對于寄存器自動機和時間自動機的模型學習的方法，并提出了一種對于時間自動機進行學習模仿的算法思想，最后對于模型學習的主要研究方向進行了闡述。

關鍵詞：模型學習；形式化方法；時間自動機；寄存器自動機

中圖分類號：TP311 文獻標識碼：A

文章編號：1009-3044（2019）10-0171-03

開放科學（資源服務）標識碼（OSID）：

1 引言

任何一個軟硬件系統在開發之前都有一個事先預定的系統規約，然后根據系統的需求進行設計和開發。最后經過測試才能保證系統能夠一定程度上完成需求規約中描述的功能和行為。如果我們想要對一個系統進行分析，可以采取在需求文檔階段進行仿真的方法，也可以對開發后的真實系統進行實際的測試分析。當用形式化的方法分析一個軟硬件系統時，學者們希望通過某種手段推斷系統的抽象模型，然后根據模型檢驗來對系統的行為進行分析。模型學習的目標是通過用觀察得到的系統行為序列和相關的數據來構建軟件和硬件系統的狀態圖模型，可以解決上述的系統模型建立問題。其中涉及的模型學習算法的設計和實現是一個非常具有研究價值的問題。從理論角度分析，這種形式化的方法更具有可信度和完備性。

本文對于近十年來可用性強的一些模型學習算法進行了匯總，其中設計的模型主要分為確定性有限自動機模型，寄存器自動機模型和時間自動機模型。并在之后提出了一個用于學習時間自動機的框架。

2 背景

有很多推斷軟件組件模型的方法，比如分析具體代碼、挖掘系統日志、執行測試等等。也有很多不同種類的模型能支持這些推斷方法，比如馬爾可夫模型、變量之間的關系模型、類圖模型等等。本文的關注點是在一種特定類型的模型之內，即狀態圖（又稱自動機），其對于理解許多軟件系統的行為至關重要，例如安全協議、網絡協議和嵌入式控制軟件。模型推斷技術可以基于白盒或黑盒，區別在于是否需要訪問代碼。黑盒技術的優點是相對容易使用，并可以應用在我們沒有代碼訪問權限或有效的白盒工具的情況下。主動學習的技術是通過主動地對軟件進行實驗測試來完成它們的任務的技術。此外，還有被動學習的方法，其中的模型是根據軟件的許多的運行行為的集合而構建的。主動學習的優點是它能夠提供軟件組件的全部完備的行為的模型，而不像被動學習那樣僅僅提供在實際操作期間發生的某系特定運行行為的模型。

近年來，模型學習技術已經具有了許多成功應用到不同領域的實際案例，比如西門子的電信系統的回歸測試分析，法國電信的集成測試分析，在施普林格出版社線上會議服務系統的自動化測試分析，在沃爾沃科技公司的線控制動系統的需求測試分析等等。事實上，模型學習正在成為銀行卡、網絡協議、遺產軟件等領域中能夠實際使用的一種高效的漏洞尋找技術。

3 學習算法

3.1 確定性有限自動機

目前學術界對于確定性有限狀態自動機的模型學習已經有了一些不錯的研究成果。在1987 年，Angluin 發表了相關研討論文[2]，她根據 Myhill-Nerode定理（對于給定一種語言L，和一對字符串x和y，定義一個能產生區別的延續字符串z，使得兩個字符串xz和yz中只有一個屬于L。對于這樣的字符串的定義一種RL規則：如果對于x和y不存在上述的能區別的延續字符串z，則x RL y可以看出來，RL是字符串上的一種等價關系，可以利用這個關系將字符串的集合劃分為若干個等價類。）表明可以使用詢問方式來學習到有限自動機，并稱之為MAT框架。在該框架中，學習被看作是一種博弈，其中學習者模塊必須通過詢問教師模塊來推斷一個未知的狀態圖的行為。學習者的任務是通過兩種類型的詢問來學習原始模型：成員查詢：學習者詢問一個行為序列是否是能被原始自動機接收，教師使用接收或拒絕來回答。等價查詢：學習者通過成員查詢所得的行為序列集合來構建一個初步的假設模型，然后向教師詢問該假設模型與原始模型是否等價，即兩個模型對于任一行為序列的接收能力是否等同。如果情況屬實，教師回答「是」。否則教師回答「否」，并提供一個反例的行為序列來區分兩個模型，并將反例返回給學習者。學習者通過反例繼續修改假設模型，繼續以上兩種提問，直到教師對于等價查詢回答「是」。

Angluin提出的L*算法的設計能夠通過多項式數量級（多項式數的大小對應于規范的自動機的規模）的復雜度的成員查詢和等價查詢來學習自動機。L*算法只是一種簡單的設計和表達，而后來更多學者對這個算法進行了擴展和優化，但是MAT框架依然是一種有效的模型學習框架。

3.2 寄存器自動機

盡管學習自動機模型的基本算法研究工作已經取得了進展，但是這些算法只能處理規模比較小的有限狀態自動機，而且很難應用于實際的系統分析。能初步應用于部分領域的一種自動機模型稱為寄存器自動機，這種自動機模型能夠存儲中間過程中產生的數據值，實現對數據流的部分操作，能夠用于描述一部分實際系統的操作行為，比如模擬一個存儲隊列的行為。在寄存器自動機中，所有數據值都是完全對稱的（只做數據值的判等，而不對數據值進行直接修改），在學習算法中可以利用這種對稱性。在寄存器自動機的模型學習過程中，比較重要的一點是如何處理一個數據語句中那些需要被存入寄存器的值，因為這些值很可能之后要被用來與參數值進行比較或者用作輸出。

Sofia Cassel等人定義了一種可以滿足Mihill Nerode定理的特殊的寄存器自動機，并提出了對應這種自動機的模型學習算法SL*[3，4]。模型學習算法通常依賴于這種右同余關系來識別學習自動機的狀態和遷移：如果兩個語句的剩余語言一致，則這兩個語句會到達同一狀態。其基本思想是為寄存器自動機定義類似Nerode的同余，用來推斷確定自動機的狀態，遷移上的寄存器約束和遷移上寄存器的賦值。該算法利用了觀察表以及自動機的對稱性質，實現的基礎數據結構被稱為符號決策樹。

學習寄存器自動機的另一種實用的方法[5]，是Aarts等人在軟件工具Tomte中實現的。一種確定性的右不變的寄存器自動機，也是基于右同余的關系進行學習。Tomte能夠支持學習帶輸入輸出的寄存器自動機，整個算法需要多個輔助模塊：原始的學習者可以學習構建一個有限的確定性Mealy機，再利用抽象模塊可以學習一個限制種類的寄存器自動機，而預兆先知模塊讓學習種類更加寬泛的寄存器自動機成為可能，確定器模塊可以幫助學習遷移上帶有新輸出的輸入輸出寄存器自動機。整個想學習過程的設計基于映射器的思想，并且被證明是學習寄存器自動機的一種有效方法。

3.3 時間自動機

時間自動機是一個帶有有限時鐘集合的有窮狀態機，提供了一種簡單而有效的方法來描述帶有時間因素的系統狀態轉換圖，屬于混合自動機的一個重要分支。它主要用于對計算機軟件和硬件系統的時間行為進行建模和分析，比如一般的實時系統和網絡系統。對于時間自動機的檢驗目標主要集中于安全性和響應程度的性質檢驗。

瑞典烏普薩拉大學計算機系的Olga Grinchtein等人在MAT的模型學習框架下提出了對時間自動機的一個子類--確定性事件記錄自動機的學習算法LSGDERA（學習帶有明確時間監視的確定性事件記錄自動機）[6]，通過確定性事件記錄自動機與確定性有限自動機的同構性和相關的語言等價性，將學習確定性有限自動機的算法成功改進成為學習一個事件記錄自動機的算法。另外他們對于一般的事件記錄自動機，利用LSGDERA和相關的合并操作得到一個比較廣泛的學習算法。他們的算法非常有開創性，但是算法的復雜度非常高且難以實現。

之后Olga又提出用時間決策樹的方法[7]去學習一個時間確定性的事件記錄自動機，在事件記錄自動機中時鐘變量記錄的是一個事件前一次發生之后所度過的時間。對每一個事件，事件記錄自動機維護一個時鐘來保存這個時間變量。其接收的行為序列是時鐘語句，這種時鐘語句可以從一般的時間語句轉換而來。該學習算法中提出了最強后置條件的設定，根據成員詢問與等價詢問生成和修改時間決策樹，并在這個數據結構中結合最強后置條件來對狀態節點進行劃分，來產生自動機中的時間監視約束，并對統一行為的節點進行合并，最終將整個時間決策樹折疊成一個時間確定性的事件記錄自動機。它是第一個避免使用時間層域的概念來學習時間自動記錄自動機的學習算法。它的優勢在于能推廣拓展到確定性的時間自動機，有強的表達能力，但是劣勢在于高的復雜度。

荷蘭代爾夫特理工大學的Sicco Verwer等人根據Miguel Bugalho等人提出了以DFA學習的紅藍邊狀態合并算法為基礎的對于單個時鐘的實時自動機進行模型學習的啟發式狀態合并算法[8]。根據系統對于抽樣的時間行為軌跡樣本的接受與否，將樣本集合分為接受集合和拒絕集合，并根據這些行為軌跡集合生成相應的樹形結構APTA（擴增前綴樹接收結構）。在APTA的基礎上可以對其中的結點進行三類操作：合并，分離，染色。該算法根據樣本接受狀態的一致性問題制定了相應的評分制度對操作進行評分，其中分高的操作先執行。最終APTA整合成一個待時間約束的確定性自動機，該自動機是單時鐘，并且每次遷移都要重置時鐘。這個算法有一定的實用性，但是在具體的實踐應用中，開始時軌跡的樣本是事先一次性確定好的，而最終該算法學習出實時自動機模型是與最初對系統行為的抽樣緊密相關的。該算法屬于被動學習的范疇，對于一個比較復雜的系統而言，我們不可能窮盡它所有的行為抽樣，所以最終學習得到的模型和真正系統中的隱含模型很可能只是一個部分相交的關系。所以在使用這個算法時，為了得到一個更加精準的模型，就必須使最初的抽樣覆蓋更多的系統特征操作。

4 學習時間自動機的一種新方案

上面的模型學習過程有些設計到轉化的問題，將一個難以學習的自動機模型通過一定條件制約轉化成另一種較為簡單學習的自動機模型，然后再進行學習處理，會讓可學習的模型種類更加寬泛。

時間自動機是處理時間語句的自動機模型，而寄存器自動機是處理數據流語句的模型，兩種模型雖然有不同的含義，但是在幾個判定問題上具有相同的可判定性和復雜度結果。有研究[9]表明兩種模型之間在特殊的語句形式和同構關系下可以產生相互的映射，并且能夠保持一些特性，比如確定性。這使得我們可以對于其中一個種類的給定模型，計算出另一種類的結果模型，而兩個模型的接收情況是針對特殊的語句來進行對應。根據這樣的思想，我們可以將這種關系應用到對于時間自動機的學習中來，并取得了一些進展。通過將時間自動機計算生成對應的寄存器自動機，然后針對這個寄存器自動機進行模型學習，然后將學習得到的寄存器自動機模型轉化為一個時間自動機的假設模型，最后得到的這個時間模型能夠覆蓋原本給定時間自動機的所有行為。整個過程（見圖1）可以實現對原時間自動機的行為的模仿，最終時間自動機的滿足特殊語句形式的運行行為路徑可以在一定條件下還原為原本時間自動機的行為路徑。但限制在于學習過程中的教師模塊的設定較為特殊，而且最終產生的行為集合對原本的行為集合是一種包含關系。

5 研究方向

上面所有的學習過程大都無法保證我們得到的模型和原模型是完全等價的，一般是包含所有的原始自動機的行為或者不能判定。而判定等價所需要的計算力是難以達到。所以一致性的測試是非常重要的一個問題。目前已知的一個可行的方案是通過輸入語句上的概率分布應用來讓學習得到的模型更加可靠，這是一種概率近似正確的策略，能夠在保證學習結果基本可用的前提下大量減少學習過程的復雜度，缺點是可能對目標系統有其他的限制。這種策略要考慮如何在可用性和復雜度之間取得平衡，我們仍需要投入大量的研究來揭示其對真正實際系統項目的學習效果。

另外，在實際應用中對于不同的系統的情況，可以考慮制定不同的學習策略。比如在部分系統內部已知的情況下，可以縮減學習模型的范圍，可認為是白盒技術與黑盒的技術的結合使用；對于不同的系統還能使用不用的對應輔助模塊，類似之前算法中涉及的映射器模塊，可能又因為系統本身特點的不同而呈現不同的特殊定制模塊來輔助整個學習過程。定制化可能成為工業化道路上的一個有效策略，但是整個學習過程的前置代價會比較大。

6 總結

本文對于模型學習的概念進行了介紹，并對相關模型的學習算法進行了簡述，并提出了一個時間自動機的模型學習方法，最后提出了模型學習流程研究的現階段需要探索的方向。模型學習仍處于發展的階段，我們希望越來越多的學者能夠投入相關的研究工作，為模型學習的工業化提供更多的支持，這對于形式化方法的發展和軟件的有效驗證都有非常重要的意義。

參考文獻：

[1] Frits Vaandrager. Model learning[J] .Communications of the ACM， 2017，（60） 2： 86-95.

[2] Dana Angluin. Learning regular sets from queries and counterexamples[J]. Information & Computation， 1987， 75（2）：87-106.

[3] Malte Isberner， Falk Howar， and Bernhard Steffen. Learning register automata：from languages to program structures. Machine Learning， 96（1-2）：65–98， 2014.

[4] Falk Howar， Bernhard Steffen， Bengt Jonsson， and Sofia Cassel. Inferring canonical register automata. In Viktor Kuncak and Andrey Rybalchenko， editors， Verification， Model Checking， and Abstract Interpretation， volume 7148 of Lecture Notesin Computer Science， pages 251–266.Springer Berlin Heidelberg，2012.

[5] F Aarts.Tomte： Bridging the Gap between Active Learning and Real-World Systems. PhD thesis， Radboud University Nijmegen， October 2014.

[6] Grinchtein O， Jonsson B， Leucker M. Learning of event-recording automata[J]. Lecture Notes in Computer Science， 2004， 3253：379-395.

[7] Grinchtein O， Jonsson B， Pettersson P. Inference of event-recording automata using timed decision trees[J]. Lecture Notes in Computer Science， 2006， 4137：435-449.

[8] Verwer S，Weerdt M D，Witteveen C.An algorithm for learning real-time automata[J].Proceedings of the BENELEARN，2007，pp.33-42.

[9] Figueira D， Hofman P ， Lasota S. Relating timed and register automata[J].Mathematical Structures in Computer Science， 2016， 26（06）：993-1021.

【通聯編輯：梁書】