First-Order and Temporal Logics for Nested Words

Rajeev Alur, Marcelo Arenas, Pablo Barcelo, Kousha Etessami, Neil Immerman, Leonid Libkin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publication22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings
Place of PublicationWashington, DC, USA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages10
Publication statusPublished - 2007

Publication series

NameLICS '07
PublisherIEEE Computer Society


Dive into the research topics of 'First-Order and Temporal Logics for Nested Words'. Together they form a unique fingerprint.

Cite this