Paper: First-Order and Temporal Logics for Nested Words (at LICS 2007)

Authors: Rajeev Alur Marcelo Arenas Pablo Barceló Kousha Etessami Neil Immerman Leonid Libkin

Abstract

Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. We provide new temporal logics for finite and infinite nested words, which are natural extensions of LTL, and prove that these logics are first-order expressively-complete. One of them is based on adding a "within" modality, evaluating a formula on a subword, to a logic CaRet previously studied in the context of verifying properties of recursive state machines. The other logic is based on the notion of a summary path that combines the linear and nesting structures. For that logic, both model-checking and satisfiability are shown to be EXPTIME-complete. Finally, we prove that first-order logic over nested words has the three-variable property, and we present a temporal logic for nested words which is complete for the twovariable fragment of first-order.

BibTeX

  @InProceedings{AlurArenasBarcelEte-FirstOrderandTempor,
    author = 	 {Rajeev Alur and Marcelo Arenas and Pablo Barceló and Kousha Etessami and Neil Immerman and Leonid Libkin},
    title = 	 {First-Order and Temporal Logics for Nested Words},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {151--160},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }