Title :
The Complexity of Verifying Ground Tree Rewrite Systems
Author :
Göller, Stefan ; Lin, Anthony Widjaja
Abstract :
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 PNEXP.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.
Keywords :
decidability; formal verification; pushdown automata; rewriting systems; trees (mathematics); EF logic; Mayr´s PRS hierarchy; PNEXP; bisimilarity checking; coNEXP; finite system; ground tree rewrite system verification; infinite systems; model checking complexity; nonelementary complexity; process rewrite system; pushdown systems; regular GTRS; syntactic fragment; Adaptation models; Automata; Complexity theory; Computational modeling; Games; Polynomials; Upper bound; Bisimulation equivalence; Complexity; Ground Tree Rewrite Systems; Model Checking;
Conference_Titel :
Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on
Conference_Location :
Toronto, ON
Print_ISBN :
978-1-4577-0451-2
Electronic_ISBN :
1043-6871
DOI :
10.1109/LICS.2011.36