Navegar

Colección

Datos Estadísticas

Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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