|
Published Articles >> Table of Contents >> Abstract
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
pp. 151-160
First-Order and Temporal Logics for Nested Words
Rajeev Alur, University of Pennsylvania
Marcelo Arenas, Pontificia Universidad Catolica de Chile
Pablo Barceló, Universidad de Chile
Kousha Etessami, University of Edinburgh
Neil Immerman, University of Massachusetts
Leonid Libkin, University of Edinburgh
Full Article Text:

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2007.19
Send link to a friend
| 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.
|
Additional Information
|
Citation:
Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, Leonid Libkin,
"First-Order and Temporal Logics for Nested Words,"
lics,
pp. 151-160,
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007),
2007
|
|