Abstract
We investigate in this paper the spatial logic TQL for querying semi-structured data, represented as unranked ordered trees over an infinite alphabet. This logic consists of usual Boolean connectives, spatial connectives (derived from the constructors of a tree algebra), tree variables and a fixpoint operator for recursion. Motivated by XML-oriented tasks, we investigate the guarded TQL fragment. We prove that for closed formulas this fragment is MSO-complete. In presence of tree variables, this fragment is strictly more expressive than MSO as it allows for tree (dis)equality tests, i.e. testing whether two subtrees are isomorphic or not. We devise a new class of tree automata, called TAGED, which extends tree automata with global equality and disequality constraints. We show that the satisfiability problem for guarded TQL formulas reduces to emptiness of TAGED. Then, we focus on bounded TQL formulas: intuitively, a formula is bounded if for any tree, the number of its positions where a subtree is captured by a variable is bounded. We prove this fragment to correspond with a subclass of TAGED, called bounded TAGED, for which we prove emptiness to be decidable. This implies the decidability of the bounded guarded TQL fragment. Finally, we compare bounded TAGED to a fragment of MSO extended with subtree isomorphism tests.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Benzaken, V., Castagna, G., Frisch, A.: CDuce: an XML-centric general-purpose language. In: 8th ACM International Conf. on Functional Programming, pp. 51–63 (2003)
Bogaert, B., Tison, S.: Equality and disequality constraints on direct subterms in tree automata. In: Finkel, A., Jantzen, M. (eds.) STACS 1992. LNCS, vol. 577, pp. 161–171. Springer, Heidelberg (1992)
Bojanczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data trees and xml reasoning. In: ACM 25th Symp. on Principles of database systems, pp. 10–19 (2006)
Boneva, I., Talbot, J.M., Tison, S.: Expressiveness of a spatial logic for trees. In: 20th IEEE Symposium on Logic in Computer Science, pp. 280–289 (2005)
Brüggemann-Klein, A., Murata, M., Wood, D.: Regular tree languages over non-ranked alphabets, 1998 (unpublished manuscript)
Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 597–610. Springer, Heidelberg (2002)
Cardelli, L., Ghelli, G.: TQL: A Query Language for Semistructured Data Based on the Ambient Logic. Mathematical Structures in Computer Science 14, 285–327 (2004)
Charatonik, W., Talbot, J.: The Decidability of Model Checking Mobile Ambients. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 339–354. Springer, Heidelberg (2001)
Comon, H., Cortier, V.: Tree automata with one memory, set constraints and cryptographic protocols. TCS 331(1), 143–214 (2005)
Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications, 1997 (October 1, 2002)
Dauchet, M., Caron, A.-C., Coquidé, J.-L.: Reduction properties and automata with constraints 20, 215–233 (1995)
Dawar, A., Gardner, P., Ghelli, G.: Expressiveness and complexity of graph logic. In: Information and Computation, vol. 205, pp. 263–310 (2007)
Hosoya, H., Pierce, B.C.: XDuce: A statically typed xml processing language. ACM Trans. Internet Techn. 3(2), 117–148 (2003)
Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree automata with equality constraints modulo equational theories. Research Report LSV-06-07, LSV, ENS Cachan, France (2006)
Karianto, W., Löding, C.: Unranked tree automata with sibling equalities and disequalities. In: 34th International Colloquium on Automata, Languages and Programming (2007)
Mongy, J.: Transformation de noyaux reconnaissables d’arbres. Forêts RATEG. PhD thesis, Université de Lille (1981)
Murata, M.: Hedge automata: A formal model for xml schemata. Technical report, Fuji Xerox Information Systems (1999)
Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over infinite alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol. 2136, pp. 560–572. Springer, Heidelberg (2001)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symp. on Logic in Computer Science, pp. 55–74. IEEE, Los Alamitos (2002)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Filiot, E., Talbot, JM., Tison, S. (2007). Satisfiability of a Spatial Logic with Tree Variables. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-74915-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74914-1
Online ISBN: 978-3-540-74915-8
eBook Packages: Computer ScienceComputer Science (R0)