| |
VOLUME 4, ISSUE 4, PAPER 11
|
First-Order 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 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.
|
Publication date: November 25, 2008
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-4(4:11)2008
Hit Counts: 2278 |
 Creative Commons | |
