| Summary: | 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 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-primitive-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-primitive-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.
|
|---|