The Complexity of Verifying Ground Tree Rewrite Systems

Ground tree rewrite systems (GTRS) are an extension of pushdown systems with the ability to spawn new sub threads that are hierarchically structured. In this paper, we study the following problems over GTRS:(1) model checking EF-logic, (2)weak bi similarity checking against finite systems, and (3) strong similarity against finite systems. Although they are all known to be decidable, we show that problems (1) and (2) have nonelementbisimilarityy, whereasproblem (3) is shown to be in coNEXP by finding a syntactic fragment of EFwhose model checking complexity is complete for P^NEXP.The same problems are studied over a more general but decidable extension of GTRS called regular GTRS (RGTRS), where regular rewriting is allowed. Over RGTRS we show that all three problems have non elementary complexity. We also apply our techniques to problems over PA-processes, a well-known class of infinite systems in Mayr´s PRS (Process Rewrite Systems) hierarchy. For example, strong bi similarity checking of PA-processes against finite systems is shown to be in coNEXP, yielding a first elementary upper bound for this problem.