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

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

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

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

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

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