基于量化布爾公式的超時(shí)態(tài)計(jì)算樹邏輯有界模型檢測(cè)

摘要： 超時(shí)態(tài)屬性的模型檢測(cè)是形式化驗(yàn)證的重要研究課題。超時(shí)態(tài)計(jì)算樹邏輯Hyper CTL*擴(kuò)展了計(jì)算樹邏輯CTL*,以顯式地量化系統(tǒng)多個(gè)執(zhí)行路徑上的性質(zhì)。針對(duì)Hyper CTL*模型檢測(cè)的高時(shí)間復(fù)雜度的問題,首先為Hyper CTL*提出了有界模型語義,其次提出了基于量化布爾公式的Hyper CTL*有界模型檢測(cè)算法,分析了該算法的正確性,最后實(shí)現(xiàn)了Hyper CTL*有界模型檢測(cè)原... （共9頁）