藉由布林有限自動機解決有限狀態機之語言方程式

Solving Finite State Machine Language Equations via Boolean Finite Automata

謝孟洋(Meng-Yang Hsieh)

指導教授 ： 江介宏

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2022年)

https://doi.org/10.6342/NTU202200402

摘要

語言方程式可以用來系統性地定義許多問題，包含有限狀態機的電路合成、協議轉換、離散控制問題等等。有限狀態機之語言方程式是語言方程式中的一種特例。藉由操作認得方程式中的語言的有限自動機，為一種有限狀態機之語言方程式的一般性解法。在求解過程中，包含了一個步驟可能會讓有限自動機的大小呈指數型增長。布林有限自動機為一種有限自動機，並且能夠有效率的在其之上執行互補操作，所以我們有興趣嘗試使用布林有限自動機求解有限狀態機之語言方程式。我們實作了我們提出的布林有限狀態機之解法於 Berkeley Automata and Language Manipulation 軟體。實驗結果顯示我們尚有一些瓶頸無法突破，但我們證實了此解法的正確與可行性。

關鍵字

有限自動機 ； 有限狀態機 ； 語言方程式

並列摘要

Language equations can be used to formulate many problems, such as finite state machine (FSM) synthesis, protocol conversion, descrete control, etc. FSM language equation problem is one of the special cases of language equation problem. Manipulating the automata recognizing the languages is a general procedure to find the solution X of the FSM language equation F • X ⊆ S. The procedure of solving X contains determinization, which may exponentially increase the size of automata. Boolean finite automata (BFA) is a kind of automata which can be efficiently complemented, so we are interested in using BFA to solve the FSM. We implement our BFA approach in Berkeley Automata and Language Manipulation (BALM) software. Experimentally, for now, we still find it hard to break through certian bottlenecks; however, we’ve definitely shown the correctness and feasibility of this approach.

並列關鍵字

finite automata ； finite state machine ； language equation

參考文獻

[1] Philip Merlin and Gregor V Bochmann. On the construction of submodule specifications and communication protocols. ACM Transactions on Programming Languages and Systems (TOPLAS), 5(1):1–25, 1983.

[2] Esfandiar Haghverdi and Hasan Ural. Submodule construction from concurrent system specifications. Information and Software Technology, 41(8):499–506, 1999.

[3] Yosinori Watanabe and Robert K Brayton. The maximum set of permissible behaviors for FSM networks. In Proceedings of International Conference on Computer Aided Design (ICCAD), pages 316–320. IEEE, 1993.

[4] Adnan Aziz, Felice Balarin, Robert K Brayton, Marika Domenica DiBenedetto, Alexander Saldanha, and Alberto L Sangiovanni-Vincentelli. Supervisory control of finite state machines. In Proceedings of International Conference on Computer Aided Verification (CAV), pages 279–292. Springer, 1995.

[5] Joachim Parrow. Submodule construction as equation solving in CCS. Theoretical Computer Science, 68(2):175–202, 1989.