Logics on Words and Trees with Data

Diego Figueira and Ranko Lazić

  • Area: LoCo
  • Level: A
  • Week: 2
  • Time: 11:00 – 12:30
  • Room: C2.01

Abstract

This course will present several results linking logics for semistructured data (such as XML) with counter systems. The course will focus on two well-studied data models: data words, and data trees. These are words and trees whose every element carries a label from a finite alphabet and a data value from an infinite domain; indeed these are standard abstractions for semi-structured documents. The focus is on the complexity and decidability of reasoning on these structures. The plan is to show three groups of logics with very differing expressive power and capabilities, in order to give an overall idea of the state of the art and different powerful techniques for proving decidability in the area. These logics are divided into: first-order logics, temporal logics, and path logics.

The course material should be useful to anyone with an interest in query languages for semi-structured data, counter systems or more generally on verification of infinite-state systems. This course has some technically demanding parts, and should appeal mainly to an audience from Logic, Verification and Theoretical Computer Science.

Slides

Introduction:

  • Words and trees with data
  • Overview of reasoning formalisms
  • Automata with counters, decidable and undecidable problems

Words:

  • First-order logic with 2 variables
  • Linear temporal logic with the freeze quantifier
  • Class-memory automata, alternating register automata
  • Connections to automata with counters
  • Infinite data words

Additional References