First-Order and Temporal Logics for Nested Words

10 years 4 months ago
First-Order and Temporal Logics for Nested Words
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 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. 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 ...
Rajeev Alur, Marcelo Arenas, Pablo Barceló,
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where LICS
Authors Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, Leonid Libkin
Comments (0)