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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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
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)
Che, D.: An efficient algorithm for tree pattern query minimization under broad integrity constraints. Int. J. Web Inform. Syst. 3(3), 231–256 (2007)
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)
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)
Li, H., Liao, H.S., Su, H.: Optimize twig query pattern based on XML schema. J. Softw. 8(6), 1479–1486 (2013)
Huth, M., Ryan, M.: Logic in Computer Science, 2nd edn., pp. 207–216. Cambridge University Press, Cambridge (2005)
Kalvala, S., Warburton, R., Lacey, D.: Program transformations using temporal logic side conditions. ACM Trans. Program. Lang. Syst. (TOPLAS) 31(4), 824–833 (2009)
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)
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)
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
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
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
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)
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
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
Kupferman, O., Pnueli, A.: Once and for all. In: Proceedings of the 10th LICS, pp. 25–35
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
Pistore, M., Vardi, M.Y.: The planning spectrum - one, two, three, infinity. In: Proceedings of the 18th LICS, pp. 234–243
Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proceedings of the 21th LICS, pp. 265–274
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)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights 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)