The Termination And Boundedness Problems Of Well-structured Pushdown Systems

In the area of formal verification,pushdown systems model single-thread recursive programs and well-structured transition systems,such as vector addition systems,are useful to represent non-recursive multi-thread programs.To satisfy the need of the analysis of recursive multi-thread programs,Cai and Ogawa propose a framework of well-structured pushdown systems(WSPDSs)to model recursive multi-thread programs[1].WSPDSs can be seen as the combination of pushdown systems and well-structured transition systems: it extends pushdown systems with both well-quasi-ordered(possibly infinitely many)states and stack alphabet;it extends well-structured pushdown systems by equipping them with a stack.The expressiveness of WSPDSs is very powerful.However,the decidability of many model checking problems of WSPDS are still open problems.In this paper,we study the termination and boundedness problems of WSPDSs:· We extend the reduced reachability tree algorithm [2] to prove the decidability of termination and boundedness of WSPDSs.We proved that a WSPDS has an infinite run if and only if its reduced reachability tree contains a pumpable node and a strict WSPDS has an infinite reachability set if and only if its reduced reachability tree contains a strictly pumpable node.· We propose an alternative algorithm based on Post*-automata to prove the decidability of termination and boundedness of WSPDSs: a WSPDS non-terminates if and only if its reduced Post*-automaton contains a pumpable edge and a strict WSPDS is unbounded if and only if its reduced Post*-automaton contains a strictly pumpable edge.· By abstracting the configuration paths to nested sequences and adopting properties of nested sequences,we prove that the upper bound of the size of the reduced reachability tree is hyper-Ackermannian for bounded WSPDSs;The lower bound is obtained from the lower bound of a subclass of bounded WSPDSs.· We prove that the reduced reachability tree of a WSPDS contains a pumpable node if and only if its reduced Post*-automaton contains a pumpable edge and also prove that the upper and lower bound of the size of its reduced reachability tree and reduced Post*-automaton is the same.· To compare these two kinds of algorithms,we propose a random WSPDS generator to construct testing samples and run these two algorithms on these testing samples;Experimental results show that the Post*-automata algorithm shows more stable behavior,i.e.,both behave more or less the same on quick problems,but the reachability tree algorithm is sometimes slower in magnitude on complex problems.