×

PDL for ordered trees. (English) Zbl 1185.03056

Summary: This paper is about a special version of PDL, proposed by Marcus Kracht, for reasoning about sibling ordered trees. It has four basic programs corresponding to the child, parent, left- and right-sibling relations in such trees. The original motivation for this language is rooted in the field of model-theoretic syntax. Motivated by recent developments in the area of semi-structured data, and, especially, in the field of query languages for XML (eXtensible Markup Language) documents, we revisit the language. This renewed interest comes with a special focus on complexity and expressivity aspects of the language, aspects that have so far largely been ignored. We survey and derive complexity results, and spend most of the paper on the most important open question concerning the language: what is its expressive power? We approach this question from two angles: Which first-order properties can be expressed? And which second-order properties? While we are still some way from definitive answers to these questions, we discuss two first-order fragments of the PDL language for ordered trees, and show how the language can be used to express some typical (second-order) problems, like the Boolean circuit and the frontier problems.

MSC:

03B70 Logic in computer science
03B45 Modal logic (including the logic of norms)
68Q25 Analysis of algorithms and problem complexity
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] ABITEBOUL S., Data on the web (2000)
[2] ALECHINA N., Logic Journal of the IGPL 8 (3) pp 325– (2000) · Zbl 0948.03022 · doi:10.1093/jigpal/8.3.325
[3] ALECHINA N., Journal of Logic and Computation 13 pp 1– (2003) · Zbl 1093.68032 · doi:10.1093/logcom/13.6.939
[4] BLACKBURN P., Logic Journal of the IGPL 2 pp 3– (1994) · Zbl 0810.03022 · doi:10.1093/jigpal/2.1.3
[5] BLACKBURN P., Computer Science Logic, vol. 1092 of LNCS pp 86– (1996)
[6] DOI: 10.1017/CBO9781107050884 · doi:10.1017/CBO9781107050884
[7] BLACKBURN P., Proceedings of Mathematics of Language (MOL–8) (2003)
[8] CONSORTIUM W.-W. W., Extensible Markup Language (XML) 1.0 (Second Edition) W3C (2004)
[9] ETESSAMI K., Proc. LICS’97 pp 228–
[10] DOI: 10.1016/0022-0000(79)90046-1 · Zbl 0408.03014 · doi:10.1016/0022-0000(79)90046-1
[11] GABBAY D., Handbook of Philosophical Logic 2 (1984) · Zbl 0572.03003 · doi:10.1007/978-94-009-6259-0
[12] GOTTLOB G., PODS’02 pp 17– (2002) · doi:10.1145/543613.543617
[13] HAREL D., Dynamic Logic (2000)
[14] KAMP J., Tense Logic and the Theory of Linear Order (1968)
[15] DOI: 10.1007/BF01048404 · Zbl 0833.03009 · doi:10.1007/BF01048404
[16] KRACHT M., Logical Aspects of Computational Linguistics pp 43– (1997) · doi:10.1007/BFb0052150
[17] KRACHT M., Tools and Techniques in Modal Logic (1999)
[18] MARX M., Proceedings of PODS’04 pp 13–
[19] MARX M., TDM’04 workshop on XML Databases and Information Retrieval (2004)
[20] MARX M., Proc. ICDT 2005, vol. 3363 of LNCS pp 114–
[21] NEVEN F., Proc. PODS pp 145–
[22] NEVEN F., Automata, Languages and Programming, Proceedings, ICALP 2000, LNCS 1853 pp 547–
[23] PALM A., Transforming tree constraints into formal grammars (1997)
[24] PALM A., Sixth Meeting on Mathematics of Language
[25] PRATT V., Proceedings of the 20th IEEE symposium on Foundations of Computer Science pp 115–
[26] ROGERS J., A Descriptive Approach to Language Theoretic Complexity (1998) · Zbl 0956.03030
[27] SPAAN E., Complexity of modal logics (1993) · Zbl 0831.03005
[28] VARDI M., Journal of Computer and System Sciences 32 pp 183– (1986) · Zbl 0622.03017 · doi:10.1016/0022-0000(86)90026-7
[29] WEYER M., Automata, Logics, and Infinite Games, vol. 2500 of LNCS pp 207– (2002) · Zbl 1021.03001 · doi:10.1007/3-540-36387-4_12
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.