关键词: XML，决策问题，可满足性检测

Abstract: In this paper, a new algorithm was proposed to analyze the decision problem to XPath in XML data which is represented as regular tree. By this way we could also check the static data's type of XPath. Based on the decidability of a logic with converse for finite ordered tree,we proved that its' time complexity is a simple exponential of the size of a formula. Then a practical and effective mathematical model was built to slow the satisfiability problem of a formula.Through some examples of decision problems, such as XPath emptiness, containment, overlap, and coverage, with or without type constraints, the algorithm was confirmed by these experiments that our system can be effectively used in static analyzers for both XPath expressions and XMI. type annotations.

Key words: XML,Decision problem,Satisfiabifity-testing