Abstract: As an important aspect of XML query optimization－Twig pattern minimizing,usually needs to take advantage of the constraints of XML Schema during the minimization process,so it is called Schema features.To simplify the traditional methods of extracting Schema features,and to ensure the accuracy of the extraction process,we proposed a model-checking algorithm to extract XML Schema features automatically.Based on the formal model of an XML Schema,we used an extended CTL formula to express Schema features,and proposed an algorithm to check if an XML Schema model satisfies CTL formula.Due to the expansion of CTL formulas,the proposed algorithm can not only express the prior Schema features,but also represent parents,ancestors and other backward features.Finally,we realizaed a aids tool for our methods.

Key words: XML schema features,Model checking,Temporal logic