Computer Science – Logic in Computer Science
Scientific paper
2008-11-04
LMCS 4 (4:11) 2008
Computer Science
Logic in Computer Science
revised and corrected version of Mar 03, 2011
Scientific paper
10.2168/LMCS-4(4:11)2008
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.
Alur Rajeev
Arenas Marcelo
Barceló Pablo
Etessami Kousha
Immerman Neil
No associations
LandOfFree
First-Order and Temporal Logics for Nested Words does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with First-Order and Temporal Logics for Nested Words, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and First-Order and Temporal Logics for Nested Words will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-184423