| In the area of programming analysis, model checking technique iswidely used, single-thread programs are well studied, but as recursivemulti-thread programs are undecidable, the research of concurrentprogramming analysis is quite a hot topic. Combining the ideas ofPushdown System(PDS) and Well-Structured Transition System, Cai andOgawa investigated a new model, which is called Well-StructuredPushdown System(WSPDS).It is a pushdown system with control statesand stack alphabets which are well-quasi-order.This paper focused on subclasses of WSPDS, in which theircoverabilities are decidable. By applying WSTS-like techniques onclassical P-automaton, two Algorithms are implemented to resolve thedecidability, in forward and backward ways. We call them Forwardalgorithm and Backward algorithm. We show some technique to solve theP-automata convergence problem in WSPDS. In the Forward one, wechoose Karp-Miller acceleration, and in the Backward one, we use Idealrepresentation. In order to improve these two algorithms’ performance,we introduce some simple structure and concepts, such as Expansion Unit.In the end, we’ll show some examples solved by the algorithms anddiscuss some performance problems. |
