DocumentCode :
2545572
Title :
The Complexity of Verifying Ground Tree Rewrite Systems
Author :
Göller, Stefan ; Lin, Anthony Widjaja
fYear :
2011
fDate :
21-24 June 2011
Firstpage :
279
Lastpage :
288
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;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on
Conference_Location :
Toronto, ON
ISSN :
1043-6871
Print_ISBN :
978-1-4577-0451-2
Electronic_ISBN :
1043-6871
Type :
conf
DOI :
10.1109/LICS.2011.36
Filename :
5970253
Link To Document :
بازگشت