Efficient evaluation for a temporal logic on changing XML documents

Conference object, Article English OPEN
Bojańczyk , Mikołaj ; Figueira , Diego (2011)
  • Publisher: ACM Press
  • Related identifiers: doi: 10.1145/1989284.1989317
  • Subject: Algorithms | Languages | Keywords | temporal logic | Query languages | General Terms | poral logic | F41 [Mathematical logic and formal languages]: Tem- | [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | H23 [Database management]: Languages— | Incremental evaluation | [ INFO.INFO-DB ] Computer Science [cs]/Databases [cs.DB] | XML | Theory
    acm: ComputingMethodologies_DOCUMENTANDTEXTPROCESSING

International audience; We consider a sequence t1,. .. , tk of XML documents that is produced by a sequence of local edit operations. To describe properties of such a sequence, we use a temporal logic. The logic can navigate both in time and in the document, e.g. a formula can say that every node with label a eventually gets a descendant with label b. For every fixed formula, we provide an evaluation algorithm that works in time O(k·log(n)), where k is the number of edit operations and n is the maximal size of document that is produced. In the algorithm, we represent formulas of the logic by a kind of automaton, which works on sequences of documents. The algorithm works on XML documents of bounded depth.
  • References (13)
    13 references, page 1 of 2

    [1] Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d'Orso, and Mayank Saksena. Regular model checking for LTL(MSO). In CAV, volume 3114 of Lecture Notes in Computer Science, pages 348{360. Springer, 2004.

    [2] Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. A survey of regular model checking. In CONCUR, volume 3170 of Lecture Notes in Computer Science, pages 35{48. Springer, 2004.

    [3] Serge Abiteboul, Laurent Herr, and Jan Van den Bussche. Temporal connectives versus explicit timestamps to query temporal databases. J. Comput. Syst. Sci., 58(1):54{68, 1999.

    [4] Andrey Balmin, Yannis Papakonstantinou, and Victor Vianu. Incremental validation of XML documents. ACM Trans. Database Syst., 29(4):710{751, 2004.

    [5] Denilson Barbosa, Alberto O. Mendelzon, Leonid Libkin, Laurent Mignet, and Marcelo Arenas. E cient incremental validation of XML documents. In ICDE, pages 671{682, 2004.

    [6] Henrik Bjorklund, Wouter Gelade, Marcel Marquardt, and Wim Martens. Incremental XPath evaluation. In ICDT, pages 162{173, 2009.

    [7] M. Bojanczyk and I. Walukiewicz. Forest algebras. In Automata and Logic: History and Perspectives, pages 107{132. Amsterdam University Press, 2007.

    [8] Mikolaj Bojanczyk and Pawel Parys. XPath evaluation in linear time. In PODS, pages 241{250, 2008.

    [9] Ghislain Fourny, Daniela Florescu, Donald Kossmann, and Markos Zacharioudakis. A time machine for XML: PUL composition. In XML Prague, 2010.

    [10] David Gabelaia, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. Products of 'transitive' modal logics. J. Symb. Log., 70(3):993{1021, 2005.

  • Metrics
    No metrics available
Share - Bookmark