Abstract:
We study the expressive power of the downward and vertical fragments of XPath equipped with (in)equality tests over possibly infinite data trees. We introduce a suitable notion of saturation with respect to node expressions, and show that over saturated data trees, the already studied notion of (unary) bisimulation coincides with the idea of ‘indistinguishability by means of node expressions’. We also prove definability and separation theorems for classes of pointed data trees. We introduce new notions of binary bisimulations, which relate two pairs of nodes of data trees. We show that over finitely branching data trees, these notions correspond to the idea of ‘indistinguishability by means of path expressions’. We prove a characterization theorem, which describes when a first-order formula with two free variables is expressible in the downward fragment. We show definability and separation theorems, for classes of two-pointed data trees and in the context of path expressions. © 2017 Elsevier Inc.
Registro:
Documento: |
Artículo
|
Título: | Model theory of XPath on data trees. Part II: Binary bisimulation and definability |
Autor: | Abriola, S.; Descotte, M.E.; Figueira, S. |
Filiación: | Universidad de Buenos Aires, Facultad de Ciencias Exactas y Naturales, Departamento de Computación, Buenos Aires, Argentina CONICET-Universidad de Buenos Aires, Instituto de Investigación en Ciencias de la Computación (ICC), Buenos Aires, Argentina Universidad de Buenos Aires, Facultad de Ciencias Exactas y Naturales, Departamento de Matemática, Buenos Aires, Argentina IMAS-UBA-CONICET, Argentina
|
Palabras clave: | Binary trees; Bins; Fault tolerance; Forestry; Characterization theorems; Equality tests; Expressive power; First-order formulas; Free variable; Indistinguishability; Path expressions; Separation theorem; Trees (mathematics) |
Año: | 2017
|
Volumen: | 255
|
Página de inicio: | 195
|
Página de fin: | 223
|
DOI: |
http://dx.doi.org/10.1016/j.ic.2017.01.002 |
Título revista: | Information and Computation
|
Título revista abreviado: | Inf Comput
|
ISSN: | 08905401
|
CODEN: | INFCE
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_08905401_v255_n_p195_Abriola |
Referencias:
- Areces, C., Carreiro, F., Figueira, S., Characterization, definability and separation via saturated models (2014) Theor. Comput. Sci., 537, pp. 72-86
- Blackburn, P., de Rijke, M., Venema, Y., Modal Logic (2001) Camb. Tracts Theor. Comput. Sci., 53. , Cambridge University Press
- Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., Two-variable logic on data trees and XML reasoning (2009) J. ACM, 56 (3), pp. 1-48
- Chang, C.C., Keisler, H.J., Model Theory (1990) Stud. Logic Found. Math., , North-Holland
- Clark, J., DeRose, S., XML path language (XPath) http://www.w3.org/TR/xpath, Website, 1999, W3C Recommendation; Dawar, A., Otto, M., Modal characterisation theorems over special classes of frames (2009) Ann. Pure Appl. Log., 161 (1), pp. 1-42
- de Rijke, M., Modal Model Theory (1995), Technical Report CS-R9517 CWI Amsterdam; de Rijke, M., Sturm, H., Global definability in basic modal logic (2001) Essays on Non-classical Logic, 1, pp. 111-135
- Figueira, D., Figueira, S., Areces, C., Model theory of XPath on data trees. Part I: bisimulation and characterization (2015) J. Artif. Intell. Res., 53, pp. 271-314. , http://www.glyc.dc.uba.ar/santiago/papers/xpath-part1.pdf
- Figueira, D., Figueira, S., Areces, C., Basic model theory of XPath on data trees (2014) International Conference on Database Theory, pp. 50-60
- Figueira, S., Gorín, D., On the size of shortest modal descriptions (2010) Advances in Modal Logic, 8, pp. 114-132
- Fletcher, G.H.L., Gyssens, M., Leinders, D., Van den Bussche, J., Van Gucht, D., Vansummeren, S., Similarity and bisimilarity notions appropriate for characterizing indistinguishability in fragments of the calculus of relations (2015) J. Log. Comput., 25 (3), pp. 549-580. , (published online 2014)
- Forti, M., Honsell, F., Set theory with free construction principles (1983) Ann. Sc. Norm. Super. Pisa, 10 (3), pp. 493-522
- Gottlob, G., Koch, C., Pichler, R., Efficient algorithms for processing XPath queries (2005) ACM Trans. Database Syst., 30 (2), pp. 444-491
- Gyssens, M., Paredaens, J., Van Gucht, D., Fletcher, G.H.L., Structural characterizations of the semantics of XPath as navigation tool on a document (2006) PODS, pp. 318-327. , ACM
- Kurtonina, N., de Rijke, M., Bisimulations for temporal logic (1997) J. Log. Lang. Inf., 6, pp. 403-425
- Kurtonina, N., de Rijke, M., Simulating without negation (1997) J. Log. Comput., 7, pp. 503-524
- Marx, M., de Rijke, M., Semantic characterizations of navigational XPath (2005) SIGMOD Rec., 34 (2), pp. 41-46
- Milner, R., A Calculus of Communicating Systems (1980) Lect. Notes Comput. Sci., 92. , Springer
- Otto, M., Elementary Proof of the van Benthem–Rosen Characterisation Theorem (2004), Technical Report 2342 Fachbereich Mathematik, Technische Universität Darmstadt; Otto, M., Bisimulation invariance and finite models (2006) Logic Colloquium '02, Lect. Notes Logic, 27, pp. 276-298
- Park, D., Concurrency and automata on infinite sequences (1981) Theoretical Computer Science, Lect. Notes Comput. Sci., 104, pp. 167-183. , Springer
- Rosen, E., Modal logic over finite structures (1997) J. Log. Lang. Inf., 6 (4), pp. 427-439
- Sangiorgi, D., On the origins of bisimulation and coinduction (2009) ACM Trans. Program. Lang. Syst., 31 (4)
- ten Cate, B., The expressivity of XPath with transitive closure (2006) PODS, pp. 328-337. , Stijn Vansummeren ACM
- van Benthem, J., Modal Correspondence Theory (1976), PhD thesis Universiteit van Amsterdam
Citas:
---------- APA ----------
Abriola, S., Descotte, M.E. & Figueira, S.
(2017)
. Model theory of XPath on data trees. Part II: Binary bisimulation and definability. Information and Computation, 255, 195-223.
http://dx.doi.org/10.1016/j.ic.2017.01.002---------- CHICAGO ----------
Abriola, S., Descotte, M.E., Figueira, S.
"Model theory of XPath on data trees. Part II: Binary bisimulation and definability"
. Information and Computation 255
(2017) : 195-223.
http://dx.doi.org/10.1016/j.ic.2017.01.002---------- MLA ----------
Abriola, S., Descotte, M.E., Figueira, S.
"Model theory of XPath on data trees. Part II: Binary bisimulation and definability"
. Information and Computation, vol. 255, 2017, pp. 195-223.
http://dx.doi.org/10.1016/j.ic.2017.01.002---------- VANCOUVER ----------
Abriola, S., Descotte, M.E., Figueira, S. Model theory of XPath on data trees. Part II: Binary bisimulation and definability. Inf Comput. 2017;255:195-223.
http://dx.doi.org/10.1016/j.ic.2017.01.002