Well-Structured下推自動(dòng)機(jī)可達(dá)性判定算法研究.pdf

1、在程序分析領(lǐng)域，模型檢測技術(shù)被廣泛應(yīng)用，單線程程序的模擬已被深入研究，而由于多線程并行程序是不可判定的，所以多線程并行程序的建模一直是一個(gè)開放且熱門的話題。通常，我們使用下推自動(dòng)機(jī)（PDS）來對(duì)單線程遞歸程序進(jìn)行建模，而對(duì)于非遞歸多線程程序的建模一般采用Well-Structured Transition System（WSTS）。近年, Cai和Ogawa將 PDS與WSTS二者結(jié)合提出了Well-StructuredPushdown

2、 Systems（WSPDS）并進(jìn)行了深入的研究。WSPDS是下推系統(tǒng)基礎(chǔ)上將控制狀態(tài)和棧字母表擴(kuò)展為well-quasi-order（普通下推系統(tǒng)為有限的），具有不錯(cuò)的表達(dá)能力，之前被深入研究的Recursive Vector Addition System with Stats（RVASS）, Multi-set Pushdown Systems（Multi-set PDS）都可以應(yīng)用該模型驗(yàn)證。
　　本文對(duì)可達(dá)性可判定的WS

3、PDS進(jìn)行了可達(dá)性算法的設(shè)計(jì)與實(shí)現(xiàn)。首先，在理論上對(duì)兩種可達(dá)性算法：Forward和Backward算法進(jìn)行了細(xì)致的分析，對(duì)其正確性做出了簡單的說明，其中，F(xiàn)orward算法在經(jīng)典的Post*-automata算法上利用Karp-Miller acceleration使得算法能夠結(jié)束；Backward算法則利用Ideal Presentation使得經(jīng)典的Pre*-automata算法能夠在WSPDS上收斂。其次，我們提出了有效的WSP