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

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

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