
VOLUME 4, ISSUE 4, PAPER 11
FirstOrder and Temporal Logics for Nested Words

©Rajeev Alur, UPenn ©Marcelo Arenas, PUC, Chile ©Pablo Barcelo, U Chile ©Kousha Etessami, U Edinburgh ©Neil Immerman, UMass ©Leonid Libkin, Edinbugh 
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 treestructured 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 firstorder
expressivelycomplete. 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
EXPTIMEcomplete, and that modelchecking 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 EXPTIMEcomplete).
Finally, we prove that firstorder logic over nested words has the
threevariable property, and we present a temporal logic for nested words which
is complete for the twovariable fragment of firstorder.

Publication date: November 25, 2008 arxiv:0811.0537v1
Corrected Version from: March 03, 2011
Full Text: PDF  PostScript DOI: 10.2168/LMCS4(4:11)2008
Hit Counts: 7861 
Creative Commons  