包含字串樹：一種用於損耗性頻道系統反向分析的資料結構

Covering Sequence Trees: A Data Structure for Backward Reachability Analysis of Lossy Channel Systems

許華祐(Hwa-You Hsu)

指導教授 ： 顏嗣鈞

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

https://doi.org/10.6342/NTU.2004.10254

摘要

損耗性頻道通訊系統（Lossy Channel Communication Systems，LCS）是一種常用於模擬自然界通訊環境的模型。通常由數個有限狀態自動機（Finite State Automata）和數個不可靠的通訊頻道所組成。在[AJ96]中，我們知道損耗性頻道通訊系統上的反向到達驗證問題（Backward Reachability Problems）是可決定的（Decidable）。[AAB99]則首先提出了一種用於損耗性頻道通訊系統的符號式驗證資料結構。在本論文中，我們提出了一種新的資料結構，包含字串樹。其特性是在表達損耗性頻道通訊系統的系統狀態的元素之間，能夠共用部分資訊，希望能達到節省記憶體空間的目的。

關鍵字

向上封閉集合 ； 損耗性頻道系統 ； 反向分析

並列摘要

無資料

並列關鍵字

LCS ； Backward Analysis ； Lossy Channel Systems ； Upward-closed Sets

參考文獻

[Ab01] P. A. Abdulla. Lossy Channel Systems. On-line lecture notes. http://www.docs.uu.se/docs/avds/lecture_notes/infstate_verification/lecture2.ps

[AAB99] P. A. Abdulla, A. Annichini, and A. Bouajjani. Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. In Proc of TACAS'99, LNCS 1579, pp 208-222, 1999.

[AABJ04] P. A. Abdulla, A. Annichini, A. Bouajjani, and B. Jonsson. Using Forward Reachability Analysis for Verification of Lossy Channel System. To appear in Int. Journal on Formal Methods in System Design

[ABJ98] P. A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. In CAV’98, LNCS 1427, 1998

[ACJT96] P. A. Abdulla, K. Cerans, B. Jonsson, and T. -K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc of LICS’96, pp313-321, 1996