Iteration-free CPDL的符號(hào)判定算法及應(yīng)用研究.pdf

1、命題動(dòng)態(tài)邏輯(PDL)是一種應(yīng)用模態(tài)邏輯,用于程序行為的推理。Iteration-free CPDL是一種無迭代算子而含有逆算子的命題動(dòng)態(tài)邏輯。包括Iteration-free CPDL在內(nèi)的各種命題動(dòng)態(tài)邏輯在程序性質(zhì)的分析以及動(dòng)作的刻畫和推理等方面具有重要的應(yīng)用價(jià)值。
　　命題動(dòng)態(tài)邏輯中一個(gè)基本的推理問題是檢查公式的可滿足性,別的推理問題通常可規(guī)約到這一問題?，F(xiàn)有的可滿足性算法是通常是基于Tableau來實(shí)現(xiàn)的。有序二叉決策圖(

2、OBDD)是一種有效地表示和處理大規(guī)模問題的數(shù)據(jù)結(jié)構(gòu),在大規(guī)模模型檢測和驗(yàn)證等領(lǐng)域已經(jīng)得到成功應(yīng)用,在邏輯公式的可滿足判定方面也具有巨大的應(yīng)用潛力。為了使OBDD符號(hào)化技術(shù)應(yīng)用于命題動(dòng)態(tài)邏輯可滿足性判定,提高PDL算法的效率,本文對(duì)OBDD的Iteration-free CPDL可滿足性判定算法進(jìn)行了研究。在此基礎(chǔ)上,應(yīng)用Iteration-free CPDL去描述Web服務(wù)組合問題。本文的具體研究成果如下:
　　(1)給出了基于

3、OBDD的Iteration-free CPDL判定算法。在分析其他邏輯可滿足性判定算法的基礎(chǔ)上,重構(gòu)了公式集模型,給出了基于OBDD的Iteration-free CPDL判定算法;證明和實(shí)例驗(yàn)證該算法是正確可行的。
　　(2)設(shè)計(jì)并實(shí)現(xiàn)了Iteration-free CPDL可滿足性判定系統(tǒng)。借鑒描述邏輯概念可滿足性判定推理機(jī)的實(shí)現(xiàn)方法,設(shè)計(jì)并實(shí)現(xiàn)了Iteration-free CPDL可滿足性判定系統(tǒng),能夠?qū)teratio