XPath and Modal Logics of Finite DAG's

摘要

XPath, CTL and the modal logics proposed by Blackburn et al, Palm and Kracht are variable free formalisms to describe and reason about (finite) trees. XPath expressions evaluated at the root of a tree correspond to existential positive modal formulas. The models of XPath expressions are finite ordered trees, or in the presence of XML's ID/IDREF mechanism graphs. The ID/IDREF mechanism can be seen as a device for naming nodes. Naming devices have been studied in hybrid logic by nominals. We add nominals to the modal logic of Palm and interpret the language on directed acyclic graphs. We give an algorithm which decides the consequence problem of this logic in exponential time. This yields a complexity result for query containment of the corresponding extension of XPath.