關(guān)于直覺主義時(shí)序邏輯若干問題的研究.pdf

1、反應(yīng)式系統(tǒng)是指能對(duì)外界事件作出反應(yīng)的系統(tǒng)，其特點(diǎn)是系統(tǒng)持續(xù)與所在環(huán)境進(jìn)行交互，此類系統(tǒng)的性質(zhì)一般涉及無限行為。而運(yùn)行時(shí)驗(yàn)證是一種輕量級(jí)程序驗(yàn)證技術(shù)，需要根據(jù)系統(tǒng)當(dāng)前運(yùn)行軌跡判定系統(tǒng)是否滿足給定性質(zhì)，涉及系統(tǒng)的有限行為。眾所周知，時(shí)序邏輯是描述反應(yīng)式系統(tǒng)性質(zhì)的主要形式語言之一。為了兼顧有限與無限行為的性質(zhì)描述，學(xué)術(shù)界針對(duì)此類邏輯語言提出了不同的語義解釋，其中，Patrick Maier等人提出了直覺主義時(shí)序邏輯。
　　本文在直覺主義

2、時(shí)序邏輯框架下對(duì)安全性和活性性質(zhì)以及迭代布爾博弈開展研究，主要工作包括如下方面：
　　1.提出了直覺主義計(jì)算樹邏輯ICTL，比較了經(jīng)典計(jì)算樹邏輯CTL與直覺主義計(jì)算樹邏輯ICTL的表達(dá)能力。
　　2.在ICTL框架中定義了全局安全性質(zhì)和活性性質(zhì)以及存在型安全性質(zhì)和活性性質(zhì)的概念，并探究了安全性質(zhì)和活性性質(zhì)在并、交、補(bǔ)等操作下的封閉性。
　　3.證明了直覺主義計(jì)算樹邏輯中的分解定理。并給出ICTL中安全性質(zhì)和活性性質(zhì)與I