The Expressiveness Of Well-structured Pushdown Systems

Well-structured pushdown systems can be regarded as an extension of pushdown systems which are equipped with well-quasi-ordered states and well-quasi-ordered stack alphabet. As a general model, well-structured pushdown systems are powerful enough to model the behaviour of many other models. Vector addition systems are widely used,in this paper, we investigate the relationship between many extension models of vector addition systems and well-structured pushdown systems. Many problems on these models can be reduced to the corresponding problems on well-structured pushdown systems.The key contribution of this paper is as follows, by explicitly using the posttraversal order of a derivation tree, any branching vector addition system can be encoded into a well-structured pushdown system; by using explicit stacks, any recursive vector addition system with states can be encoded into a well-structured pushdown system; by storing the information of one entry of vectors into the depth of the stack,any vector addition system with one zero-test can be converted to a well-structured pushdown system.Some other models, such as one counter net, one counter automaton, alternating vector addition systems with states can be encoded into well-structured pushdown systems, too. Many problems on these models can also be converted to the corresponding problems on well-structured pushdown systems.The results of this paper are profound. The decidable results on well-structured pushdown systems can be directly applied to these models. Besides, the decidable results of these models can also act as a guide to help us ?nd more subclasses of wellstructured pushdown system that have decidable results.