良結(jié)構(gòu)下推系統(tǒng)上的可終止性和有界性問題研究.pdf

1、在形式化驗(yàn)證領(lǐng)域，下推系統(tǒng)（pushdown systems）常用來建模單線程遞歸程序，良結(jié)構(gòu)遷移系統(tǒng)（well-structured transition systems），比如向量加法系統(tǒng)（vector addition systems），常用來建模非遞歸多線程程序。結(jié)合這兩種系統(tǒng)及目前對(duì)于遞歸并發(fā)程序分析的需求，Cai和Ogawa提出了建模遞歸并發(fā)程序的框架：良結(jié)構(gòu)下推系統(tǒng)（well-structured pushdown sys

2、tems）[1]。良結(jié)構(gòu)下推系統(tǒng)可以看做是下推系統(tǒng)和良結(jié)構(gòu)遷移系統(tǒng)的結(jié)合：與下推系統(tǒng)比較，它將下推系統(tǒng)的狀態(tài)集和棧字符集從有限集擴(kuò)展為良擬序集（well quasi order）；與良結(jié)構(gòu)遷移系統(tǒng)比較，它在良結(jié)構(gòu)遷移系統(tǒng)的基礎(chǔ)上配置了一個(gè)棧。良結(jié)構(gòu)下推系統(tǒng)的表達(dá)能力十分強(qiáng)大，但其上的很多模型檢測(cè)問題的可判定性目前都還是公開問題。本文我們主要研究良結(jié)構(gòu)下推系統(tǒng)的可終止性問題及有界性問題：
　　擴(kuò)展了刪枝可達(dá)樹算法[2]證明良結(jié)構(gòu)下推

3、系統(tǒng)的可終止性和有界性問題是可判定的，在擴(kuò)展的刪枝可達(dá)樹上證明了一個(gè)良結(jié)構(gòu)下推系統(tǒng)有一條無限長的路徑當(dāng)且僅當(dāng)它的刪枝可達(dá)樹中包含一個(gè)可泵節(jié)點(diǎn)（pumpable node），一個(gè)嚴(yán)格良結(jié)構(gòu)下推系統(tǒng)的可達(dá)集是無限的當(dāng)且僅當(dāng)它的刪枝可達(dá)樹中包含一個(gè)嚴(yán)格可泵節(jié)點(diǎn)（strictly pumpable node）；
　　提出另外一種證明良結(jié)構(gòu)下推系統(tǒng)的可終止性和有界性問題的可判定性的算法：后繼自動(dòng)機(jī)算法（P ost?-automata alg

4、orithm）。證明了一個(gè)良結(jié)構(gòu)下推系統(tǒng)是不可終止的當(dāng)且僅當(dāng)它的簡化后繼自動(dòng)機(jī)（reduced P ost?-automaton）中存在一條可泵邊（pumpable edge），一個(gè)嚴(yán)格良結(jié)構(gòu)下推系統(tǒng)是無界的當(dāng)且僅當(dāng)它的簡化后繼自動(dòng)機(jī)中存在一條嚴(yán)格可泵邊（strictly pumpable edge）；
　　通過將格局遷移路徑抽象為嵌套序列（nested sequence），利用嵌套序列的一些性質(zhì)證明了良結(jié)構(gòu)下推系統(tǒng)的子模型受控良

5、結(jié)構(gòu)下推系統(tǒng)（bounded well-structured pushdown systems）的刪枝可達(dá)樹的大小的上界為高階阿克曼的（hyper-Ackermannian）；下界則由受控良結(jié)構(gòu)下推系統(tǒng)的一類子模型的下界得到，也是高階阿克曼的；
　　證明了一個(gè)良結(jié)構(gòu)下推系統(tǒng)的刪枝可達(dá)樹與簡化后繼自動(dòng)機(jī)的關(guān)系：一個(gè)良結(jié)構(gòu)下推系統(tǒng)的刪枝可達(dá)樹中包含一個(gè)可泵節(jié)點(diǎn)當(dāng)且僅當(dāng)它的簡化后繼自動(dòng)機(jī)中存在一條可泵邊。并證明了簡化后繼自動(dòng)機(jī)的大小的上