The Complexity of Verifying Ground Tree Rewrite Systems
The Complexity of Verifying Ground Tree Rewrite Systems
复制标题
DOI：
10.1109/lics.2011.36
复制
发表时间：
2011-06
期刊：
影响因子：
--
通讯作者：
Stefan Göller;A. Lin
中科院分区：
文献类型：
--
作者：
Stefan Göller;A. Lin
地面树重写系统（GTRS）是下推系统的扩展，具有生成分层结构的新子线程的能力。本文研究了GTRS上的以下问题：(1)模型检验ef -逻辑，(2)有限系统弱双相似性检验，(3)有限系统强相似性检验。虽然已知它们都是可决定的，但我们证明问题(1)和(2)具有非元素双相似性，而问题(3)通过找到一个ef的语法片段来证明在$\coNEXP$中，其模型检查复杂度对于$\P^\NEXP$是完整的。在GTRS的更一般但可确定的扩展上研究了同样的问题，称为正则GTRS (RGTRS)，其中允许正则重写。在RGTRS上，我们证明了这三个问题都具有非初等复杂性。我们还将我们的技术应用于pa过程的问题，pa过程是Mayr的PRS（过程重写系统）层次结构中众所周知的无限系统类。例如，对有限系统的pa过程的强双相似性检验被证明是在$\coNEXP$中，为这个问题产生了一个初等上界。
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.