關于直覺主義時序邏輯若干問題的研究.pdf

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

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