摘要:簡要介紹了有限精度時間自動機(FPTA)的基本概念,重點討論FPTA狀態(tài)中時鐘的表示。FPTA只記錄時鐘值的整數(shù)部分,而用時鐘序的概念來模擬表示時鐘值小數(shù)部分的大小關系,從而減少生成的狀態(tài)空間。在FPTA模型中,時鐘操作的時空性能主要依賴于時鐘序的數(shù)據(jù)結構和算法。提出了用位矩陣來表示時鐘序的數(shù)據(jù)結構POM(PartialOrder Matrix)。采用該結構的操作算法具有O(n)復雜度,且無需標準化操作;同時,一切操作均可以通過位運算實現(xiàn),從而大幅度提高時鐘操作的時間效率。
關鍵詞:有限精度時間自動機; 模型檢驗; 符號化方法
中圖法分類號:TP301.1
文獻標識碼:A
文章編號:1001-3695(2006)07-0023-03