Identifying XML Schema Constraints Using Temporal Logic

  • Ruifang ZhaoEmail author
  • Ke Liu
  • Hongli Yang
  • Zongyan Qiu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


Twig pattern minimization is an important aspect of XML query optimization. During the minimizing process, it usually needs to take advantage of the constraints of XML Schema. The traditional methods for identifying constraints is to develop corresponding algorithms based on the type of constraints. It is inflexible because the constraints may be changed as new Twig pattern optimizing rules are found. Since the constraints of XML Schema mainly depict the sequence relationship of nodes, it is natural to be described by temporal logic. Based on the recognition, this paper proposes a method of identifying XML Schema constraints using temporal logic. Concretely, an XML Schema is modeled as a graph. In order to easily represent constraints related to parent and ancestor nodes, we made some modifications to Computational Tree Logic(CTL) with backward temporal operators, and developed model checking algorithms for automatically identifying XML Schema constraints. Compared with traditional methods, our method is more flexibility.


XML Schema constraint Model checking Temporal logic 


  1. 1.
    Jagadish, H.V., Lakshmanan, L.V.S., Srivastava, D., Thompson, K.: TAX: a tree algebra for XML. In: Ghelli, G., Grahne, G. (eds.) DBPL 2001. LNCS, vol. 2397, pp. 149–164. Springer, Heidelberg (2002). doi: 10.1007/3-540-46093-4_9 CrossRefGoogle Scholar
  2. 2.
    Amer-Yahia, S., Cho, S.R., Lakshmanan, L.V.S., et al.: Tree pattern query minimization. VLDB J. Int. J. Very Large Data Bases 11(4), 315–331 (2002)CrossRefzbMATHGoogle Scholar
  3. 3.
    Che, D.: An efficient algorithm for tree pattern query minimization under broad integrity constraints. Int. J. Web Inform. Syst. 3(3), 231–256 (2007)CrossRefGoogle Scholar
  4. 4.
    Chen, D., Chan, C.Y.: Minimization of tree pattern queries with constraints. In: Proceedings of the 2008 ACM SIGMOD International Conference on Management of Data, pp. 609–622 (2008)Google Scholar
  5. 5.
    Lee, K.H., Whang, K.Y., Han, W.S.: Xmin: minimizing tree pattern queries with minimality guarantee. World Wide Web 13(3), 343–371 (2010)CrossRefGoogle Scholar
  6. 6.
    Li, H., Liao, H.S., Su, H.: Optimize twig query pattern based on XML schema. J. Softw. 8(6), 1479–1486 (2013)CrossRefGoogle Scholar
  7. 7.
    Huth, M., Ryan, M.: Logic in Computer Science, 2nd edn., pp. 207–216. Cambridge University Press, Cambridge (2005)Google Scholar
  8. 8.
    Kalvala, S., Warburton, R., Lacey, D.: Program transformations using temporal logic side conditions. ACM Trans. Program. Lang. Syst. (TOPLAS) 31(4), 824–833 (2009)CrossRefGoogle Scholar
  9. 9.
    Afanasiev, L., Franceschet, M., Marx, M., et al.: Ctl model checking for processing simple xpath queries. Proc. Temp. Represent. Reasoning 152(6), 117–124 (2004)Google Scholar
  10. 10.
    Currim, F.A., Currim, S.A., Dyreson, C.E., et al.: Adding temporal constraints to XML schema. IEEE Trans. Knowl. Data Eng. 24(8), 1361–1377 (2012)CrossRefGoogle Scholar
  11. 11.
    Libkin, L., Sirangelo, C.: Reasoning about XML with temporal logics and automata. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 97–112. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-89439-1_7 CrossRefGoogle Scholar
  12. 12.
    Libkin, L.: Logics for unranked trees: an overview. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 35–50. Springer, Heidelberg (2005). doi: 10.1007/11523468_4 CrossRefGoogle Scholar
  13. 13.
    Arenas, M., Barceló, P., Libkin, L.: Combining temporal logics for querying XML documents. In: Schwentick, T., Suciu, D. (eds.) ICDT 2007. LNCS, vol. 4353, pp. 359–373. Springer, Heidelberg (2006). doi: 10.1007/11965893_25 CrossRefGoogle Scholar
  14. 14.
    Zhang, J.M., Tao, S.Q., Liang, J.Y.: Minimization of path expression under structural integrity constraints for XML. J. Softw. 20(11), 2977–2987 (2009)CrossRefGoogle Scholar
  15. 15.
    Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–364. Springer, Heidelberg (1991). doi: 10.1007/3-540-54415-1_54 CrossRefGoogle Scholar
  16. 16.
    Hafer, T., Thomas, W.: Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 269–279. Springer, Heidelberg (1987). doi: 10.1007/3-540-18088-5_22 CrossRefGoogle Scholar
  17. 17.
    Kupferman, O., Pnueli, A.: Once and for all. In: Proceedings of the 10th LICS, pp. 25–35Google Scholar
  18. 18.
    Bozzelli, L.: The complexity of CTL* + linear past. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 186–200. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78499-9_14 CrossRefGoogle Scholar
  19. 19.
    Pistore, M., Vardi, M.Y.: The planning spectrum - one, two, three, infinity. In: Proceedings of the 18th LICS, pp. 234–243Google Scholar
  20. 20.
    Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proceedings of the 21th LICS, pp. 265–274Google Scholar
  21. 21.
  22. 22.
    Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past.In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, July 2002, pp. 383–392. IEEE Comp. Soc. Press (2002)Google Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Ruifang Zhao
    • 1
    Email author
  • Ke Liu
    • 1
  • Hongli Yang
    • 1
  • Zongyan Qiu
    • 2
  1. 1.Beijing University of TechnologyBeijingChina
  2. 2.Peking UniversityBeijingChina

Personalised recommendations