Termination and Boundedness for Well-Structured Pushdown Systems

摘要

Well-structured pushdown systems (WSPDSs) extend pushdown systems withwell-quasi-ordered (possibly infinitely many) states and stack alphabet. As an expressive model for concurrent recursive computations, WSPDSs are believed to "be close the border of undecidability"[11]. Most of the decidability results are known only on subclasses. In this paper, we investigate the decidability of the termination and boundedness problems for WSPDSs using two algorithms: One is an extension of the reduced reachability tree technique proposed by Leroux et. al in [11]. The other is based on Post*-automata technique which has been successfully applied in the model checking of pushdown systems. The complexity of both are Hyper-Ackermannian for bounded WSPDSs. We implement both algorithms and make experiments on a large number of randomly generated WSPDSs. The results illustrate thatthe Post*-automata based algorithm sometimes behaves an order of magnitude faster.