Graph Logics with Rational Relations and the Generalized Intersection Problem
Graph Logics with Rational Relations and the Generalized Intersection Problem
复制标题
DOI：
10.1109/lics.2012.23
复制
发表时间：
2012-06
期刊：
影响因子：
--
通讯作者：
P. Barceló;Diego Figueira;L. Libkin
中科院分区：
文献类型：
--
作者：
P. Barceló;Diego Figueira;L. Libkin
我们探讨了词的规则关系和理性关系相互作用的一些基本问题。主要的动机来自查询图拓扑的逻辑的研究，最近发现了许多应用。这类逻辑在由正则语言和关系表示的路径上使用条件，但它们通常需要通过诸如子字（因子）或子序列之类的有理关系来扩展。在这样的扩展图逻辑中，评估公式归结为检查有理关系与正则或可识别关系的交集的非空性（或者更一般地说，广义交集问题，询问正则关系的某些投影是否与给定的有理关系有非空交集）。我们证明了对于几个基本的和常用的有理关系，与正则关系的交集问题要么是不可判定的（例如，对于子字或后缀，以及某些推广），或者具有非多重递归复杂性的可判定（例如，子序列及其推广）。这些结果被用来排除许多类的图形逻辑，自由联合收割机定期和合理的关系，以及提供最简单的问题，验证有损耗的信道系统，具有非乘法递归的复杂性。然后，我们证明了一个二分法的结果，逻辑相结合的正规条件，对个别路径和合理的关系的路径，通过显示的语法形式的公式将它们分为有效的检查或不可判定的情况下。我们还给出了合理的关系，这种逻辑是可判定的，即使没有句法限制的例子。
We investigate some basic questions about the interaction of regular and rational relations on words. The primary motivation comes from the study of logics for querying graph topology, which have recently found numerous applications. Such logics use conditions on paths expressed by regular languages and relations, but they often need to be extended by rational relations such as subword (factor) or subsequence. Evaluating formulae in such extended graph logics boils down to checking nonemptiness of the intersection of rational relations with regular or recognizable relations (or, more generally, to the generalized intersection problem, asking whether some projections of a regular relation have a nonempty intersection with a given rational relation). We prove that for several basic and commonly used rational relations, the intersection problem with regular relations is either undecidable (e.g., for subword or suffix, and some generalizations), or decidable with non-multiply-recursive complexity (e.g., for subsequence and its generalizations). These results are used to rule out many classes of graph logics that freely combine regular and rational relations, as well as to provide the simplest problem related to verifying lossy channel systems that has non-multiply-recursive complexity. We then prove a dichotomy result for logics combining regular conditions on individual paths and rational relations on paths, by showing that the syntactic form of formulae classifies them into either efficiently checkable or undecidable cases. We also give examples of rational relations for which such logics are decidable even without syntactic restrictions.