顏嗣鈞臺灣大學：電機工程學研究所許華祐Hsu, Hwa-YouHwa-YouHsu2007-11-262018-07-062007-11-262018-07-062004http://ntur.lib.ntu.edu.tw//handle/246246/53364損耗性頻道通訊系統（Lossy Channel Communication Systems，LCS）是一種常用於模擬自然界通訊環境的模型。通常由數個有限狀態自動機（Finite State Automata）和數個不可靠的通訊頻道所組成。在[AJ96]中，我們知道損耗性頻道通訊系統上的反向到達驗證問題（Backward Reachability Problems）是可決定的（Decidable）。[AAB99]則首先提出了一種用於損耗性頻道通訊系統的符號式驗證資料結構。在本論文中，我們提出了一種新的資料結構，包含字串樹。其特性是在表達損耗性頻道通訊系統的系統狀態的元素之間，能夠共用部分資訊，希望能達到節省記憶體空間的目的。摘要………………………………………………………………………1 第一章 緒論………………………………………………………………2 1.1研究動機………………………………………………………………2 1.2 論文結構……………………………………………………………3 第二章 理論基礎…………………………………………………………4 2.1損耗性頻道通訊系統………………………………………………4 2.2良好結構狀態轉換系統………………………………………………9 2.3簡單正規描述………………………………………………………13 2.4 包含共用樹…………………………………………………………14 第三章 用於損耗性頻道通訊系統反向驗證的資料結構與演算法…17 3.1包含字串樹…………………………………………………………17 3.2將包含字串樹應用於損耗性頻道系統的驗證……………………31 3.3 共用字串樹和簡單正規描述的比較………………………………40 第四章 實驗實作與結果………………………………………………41 4.1變換位元協定………………………………………………………41 4.2領袖推舉協定………………………………………………………44 4.3 實驗結果……………………………………………………………47 第五章 結論與未來展望………………………………………………49 第六章 參考資料………………………………………………………50 附錄一 專有名詞中英對照……………………………………………52 附錄二 包含字串樹演算法時間分析…………………………………54 附錄三 計算前像投影演算法的時間分析……………………………641832409 bytesapplication/pdfen-US向上封閉集合損耗性頻道系統反向分析LCSBackward AnalysisLossy Channel SystemsUpward-closed Setsthesishttp://ntur.lib.ntu.edu.tw/bitstream/246246/53364/1/ntu-93-R91921079-1.pdf