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

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

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