Skip to main content

Identifying XML Schema Constraints Using Temporal Logic

  • Conference paper
  • First Online:
Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9984))

  • 461 Accesses

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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

    Chapter  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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. 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)

    Article  Google Scholar 

  6. Li, H., Liao, H.S., Su, H.: Optimize twig query pattern based on XML schema. J. Softw. 8(6), 1479–1486 (2013)

    Article  Google Scholar 

  7. Huth, M., Ryan, M.: Logic in Computer Science, 2nd edn., pp. 207–216. Cambridge University Press, Cambridge (2005)

    Google Scholar 

  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)

    Article  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  17. Kupferman, O., Pnueli, A.: Once and for all. In: Proceedings of the 10th LICS, pp. 25–35

    Google Scholar 

  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

    Chapter  Google Scholar 

  19. Pistore, M., Vardi, M.Y.: The planning spectrum - one, two, three, infinity. In: Proceedings of the 18th LICS, pp. 234–243

    Google Scholar 

  20. Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proceedings of the 21th LICS, pp. 265–274

    Google Scholar 

  21. http://www.lsv.ens-cachan.fr/~markey/PLTL.php

  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 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Ruifang Zhao .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Zhao, R., Liu, K., Yang, H., Qiu, Z. (2016). Identifying XML Schema Constraints Using Temporal Logic. In: Fränzle, M., Kapur, D., Zhan, N. (eds) Dependable Software Engineering: Theories, Tools, and Applications. SETTA 2016. Lecture Notes in Computer Science(), vol 9984. Springer, Cham. https://doi.org/10.1007/978-3-319-47677-3_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47677-3_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47676-6

  • Online ISBN: 978-3-319-47677-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics