LTL概率模型檢驗優(yōu)化技術(shù)的研究.pdf

1、概率模型檢驗是一種針對概率模型的形式化驗證技術(shù)，與傳統(tǒng)的非概率模型檢驗相比，概率模型檢驗不僅能對系統(tǒng)進行定性的檢驗，即判斷系統(tǒng)是否滿足某個給定的性質(zhì)，而且還能定量的對概率系統(tǒng)，或者具有概率行為的系統(tǒng)進行檢驗，即模型在哪個概率區(qū)間滿足給出的性質(zhì)。概率模型檢驗中，通常用線性時序邏輯(Linear Temporal Logic，LTL)和計算樹邏輯(Computational Tree Logic，CTL)來描述系統(tǒng)性質(zhì)。雖然LTL與CTL表

2、達能力有交集，但是如公平性性質(zhì)這樣重要的性質(zhì)只能用LTL來表示。然而，相比于CTL，當(dāng)前LTL概率模型檢驗算法的復(fù)雜度非常高，驗證效率很低，因此目前已有的概率模型工具如MRMC和PRISM均不支持對LTL性質(zhì)的驗證。
　　針對這個問題，本文提出了一種基于概率保持的公式化簡技術(shù)。該優(yōu)化技術(shù)通過縮短待驗證公式的長度來減小算法執(zhí)行的時空開銷，從而提高算法的執(zhí)行效率，在一定程度上緩解了LTL概率模型檢驗算法復(fù)雜度高的難題。
　　以上