Efficient decision procedure for a logic for xml

In this paper, we investigate formal verification techniques to solve decision
problems in the world of XML. Such problems can be uniformly modeled
by formulas of a modal logic defined on XML trees and having general least and
greatest fixpoint operators. This logic suciently captures XPath, a path language
for querying XML, and thus models type-checking problems for XPath-based
XML transformation. We then give an ecient algorithm that decides the satisfi-
ability of a formula of this logic, which is also implemented using the state-of-art
verification techniques. Our experiment verifies its eciency through real-world
XPath containment and XSLT type-checking problems.

By: Akihiko Tozawa and Masami Hagiya

Published in: RT0592 in 2007

This Research Report is not available electronically. Please request a copy from the contact listed below. IBM employees should contact ITIRC for a copy.

Questions about this service can be mailed to reports@us.ibm.com .