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