無限狀態系統之自動驗證(3/3)
Date Issued
2005-10-31
Date
2005-10-31
Author(s)
DOI
932213E002003
Abstract
在計算機科學的研究領域中，計算理論 (Theory of Computation) 具有相當悠久的
歷史。除了其本身深具困難度與挑戰性外，計算理論對於計算機科學的其他研究領
域分支，亦深具影響力。嚴格說來，計算理論提供了這些其他相關研究(compiler、
programming languages、pattern recognition、等等) 紮實的理論基礎以及分析工具。
隨著時間的演進，計算理論的研究重點也有所不同，從七、八零年代較著重於純理
論的研究(重點在automata theory、 formal languages、complexity theory、 等等) ，
演變到現今的潮流是將計算理論多年發展所累積的知識與技術，應用到real-world
problems 的解決上。這包括利用自動機理論 (automata theory)來協助電腦軟、硬
體系統的驗證(verification) ，利用 樹狀自動機 (tree automata)來提供XML 理論基
礎與其相關問題的分析描述⋯ 等等。
隨著電腦軟、硬體的複雜化，正規驗證與分析技術，近年來逐漸受到國際學術界與
工業界的重視。未來的工業產品，若不能運用自動化的分析技術來協助提升品質，
將很難保有競爭力。這個趨勢在工業界可以看到各種正規驗證技術的成功運用案
例，以及各種結合傳統與正規技術的廣泛運用；而功能驗證的技術更是大型EDA公司
（如Cadence與Synopsys）技術發展的重點。 傳統的驗證，侷限於有限狀態系統
(finite-state systems)的驗證，但近幾年的研究重點，已漸漸導向各種無限狀態系統
(infinite-state systems) 的驗證。
薄膜計算 (membrane computing)為分子計算 (molecular computing) 的一分
支， 為1998 Gh. Paun 所提出的另一類 非傳統式計算模式 (nonstandard
computational model) 。 (其他非傳統式計算模式包括國科會目前所大力推動的量
子計算 ( quantum computing)) 。 薄膜計算探討的計算模式，也是一類無限狀態
系統。
在此三年期研究計畫中， 主持人以計算理論為基礎，探討多類無限狀態系統的驗
證，獲得許多具體成果。在接下來的報告中，我們將對於研究成果逐一敘述。
Publisher
臺北市：國立臺灣大學電機工程學系暨研究所
Type
report
File(s)![Thumbnail Image]()
Loading...
Name
932213E002003.pdf
Size
262.3 KB
Format
Adobe PDF
Checksum
(MD5):4097947cf2bf3593b1892c4fe25a3c88