Rajeev Alur ; Marcelo Arenas ; Pablo Barcelo ; Kousha Etessami ; Neil Immerman et al. - First-Order and Temporal Logics for Nested Words

lmcs:782 - Logical Methods in Computer Science, November 25, 2008, Volume 4, Issue 4 - https://doi.org/10.2168/LMCS-4(4:11)2008
First-Order and Temporal Logics for Nested WordsArticle

Authors: Rajeev Alur ; Marcelo Arenas ; Pablo Barcelo ; Kousha Etessami ; Neil Immerman ; Leonid Libkin ORCID

    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 (RSMs). The other logic, NWTL, is based on the notion of a summary path that uses both the linear and nesting structures. For NWTL we show that satisfiability is EXPTIME-complete, and that model-checking can be done in time polynomial in the size of the RSM model and exponential in the size of the NWTL formula (and is also 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 two-variable fragment of first-order.


    Volume: Volume 4, Issue 4
    Published on: November 25, 2008
    Imported on: January 17, 2008
    Keywords: Computer Science - Logic in Computer Science,F.1.1, F.3.1, F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Synaptic Mechanisms for the Processing of Temporal Codes; Funder: National Science Foundation; Code: 1050701
    • Collaborative Research: Advanced Static-Analysis Techniques for Ensuring Reliable Software; Funder: National Science Foundation; Code: 0541018
    • Behavioral Interfaces for Software Components; Funder: National Science Foundation; Code: 0541149
    • Variables versus Size: Tradeoffs in Descriptive Complexity; Funder: National Science Foundation; Code: 0830174

    31 Documents citing this article

    Consultation statistics

    This page has been seen 1512 times.
    This article's PDF has been downloaded 369 times.