基于重寫邏輯的SNP系統(tǒng)模型檢測.pdf

1、隨著計算機科學與其他學科之間的相互滲透和影響，科學家們根據(jù)不同原理提出了不同的計算模型。細胞膜計算是一種基于生物細胞膜結(jié)構(gòu)和功能的新型計算模型，近年來得到廣泛的研究。SNP系統(tǒng)（Spiking Neural PSystems）是對類神經(jīng)細胞膜計算（Neural-like PSystems）的擴展。與其他細胞膜計算的不同的是，它在計算中引入了時間的概念，計算由一個全局時鐘驅(qū)動。SNP系統(tǒng)已被證明具有與圖靈機相同的計算能力。 然而隨

2、著研究的深入，模型的設計越來越復雜，如何有效地驗證模型的正確性和研究SNP系統(tǒng)的性質(zhì)成為該領域當前一個迫切需要解決的問題。模型檢測作為一種研究和驗證系統(tǒng)性質(zhì)的方法，可以有效地幫助我們解決這一問題。目前用于模型檢測的工具主要有SPIN、Maude等。Maude是一種基于重寫邏輯的形式化描述語言，由Maude解釋器解釋執(zhí)行，主要用于模型檢測和邏輯推理。 本文的主要工作是：通過擴展Maude中的重寫規(guī)則語義，利用代數(shù)方法定義了SNP系

3、統(tǒng)中計算規(guī)則的操作語義，并借助于Maude中面向?qū)ο蟮男问交枋?，給出了SNP系統(tǒng)通用的描述方法，把SN P系統(tǒng)轉(zhuǎn)化成為可執(zhí)行的形式化描述。這種形式化的描述可以被Maude解釋器解釋運行，從而自動推導系統(tǒng)的計算結(jié)果、驗證系統(tǒng)的某些性質(zhì)等。最后，本文將這一形式化描述方法應用于具體的SNP系統(tǒng)模型并給出了驗證的結(jié)果，證明了模型檢測的可行性與正確性。 本文的主要貢獻是：將模型檢測應用于SNP系統(tǒng)；利用Maude語言定義了SNP系統(tǒng)中計