First-Order and Temporal Logics for Nested Words

1. Introduction

• Nested words pair a linear execution sequence with matching call-return structure, also representing parse trees and XML-like data.The model captures sequential and hierarchical structure together.Source: §1 · p. 2
• Ordinary-word temporal logics cannot express several useful interprocedural properties, including scope-bounded requirements that are expressible in first-order logic.Tree logics often focus on hierarchy while largely ignoring linear structure.Source: §1 · pp. 2–3
• The paper seeks nested-word temporal logics combining first-order expressive completeness, reasonable model-checking and satisfiability complexity, and natural operators.These are presented as qualities desirable in a temporal logic for nested words.Source: §1 · pp. 2–3
• NWTL extends LTL with past and future Until over summary paths and supports model checking in polynomial model size and exponential formula size.The stated model-checking complexity is EXPTIME-complete.Source: §1 · p. 3
• CaRet variants with within operators are also first-order complete, but their satisfiability and model checking are 2EXPTIME-complete.They are provably more concise than NWTL, with added complexity.Source: §1 · p. 3
• Over nested words, first-order formulas with at most two free variables can be expressed using three variables, and a temporal logic captures the two-variable fragment.The paper relates the three-variable result to analogous results for words and finite trees.Source: §1 · pp. 3–4

Related Work.

• Prior tree logics often neglect linear navigation, while reconciling tree and nested-word navigation supports the expressive-completeness proof.The paper also uses logics for tree-structured data in that proof.Source: Related Work · p. 4

Organization.

• The paper is organized around notation, temporal logics, expressive completeness, model checking, and the one- and two-variable results.Source: Organization · p. 4

2.1. Nested Words.

• A nested word is a finite or infinite word equipped with a matching relation linking calls to returns under well-bracketing constraints.A finite nested word is a tuple containing the word, matching relation, and call and return predicates.Source: §2.1 · pp. 4–5
• Calls and returns may be unmatched; a well-matched nested word has no pending calls or returns.In well-matched words, the call and return predicates are uniquely determined by the matching relation.Source: §2.1 · p. 5
• First-order structures for nested words include the word order, position labels, and matching, call, and return relations.The universe is the finite set of positions or, for an infinite nested word, the natural numbers.Source: §2.1 · p. 5
• A subword induced by positions i through j is a finite nested word; for infinite nested words, the suffix from i is also defined.When j < i, the induced subword is empty.Source: §2.1 · p. 5

2.2. Games and types.

• Quantifier rank measures quantifier nesting depth, and a rank-k type records which rank-k first-order sentences hold in a structure.There are finitely many rank-k types, each definable by a first-order sentence.Source: §2.2 · pp. 5–6
• Ehrenfeucht-Fraïssé games characterize agreement on rank-k types, while k-pebble games characterize agreement for formulas using at most k variables.In an EF game, the responding player maintains a partial isomorphism; the pebble-game correspondence likewise must remain a partial isomorphism.Source: §2.2 · p. 6

3. Temporal Logics over Nested Words

• The logics combine successor and matching-call/return next and previous operators with path-dependent until and since; CaRet includes linear and abstract untils and call-since.CaRet also has matching-call/return next and a call-previous operator.Source: §3 · p. 6, §3.1 · pp. 6–7

3.1. Paths in Nested Words.

• Summary paths use successor and nesting edges to form the shortest directed route between positions, with call-skipping determined by the destination.Every pair of positions has a unique summary path.Source: §3.1 · p. 7
• Summary-down paths allow call edges, nesting edges, and internal edges, while summary-up paths allow return edges, nesting edges, and internal edges.A general summary path concatenates a summary-up path and a summary-down path.Source: §3.1 · pp. 7–8

3.2. Specifying Requirements.

• The within operator evaluates a formula on the subword of one procedure call, while summary-down paths can express scope-bounded invariants and write-read requirements.The write-read requirement requires a read along a summary-down path before another write, with no intervening write on that path or in an enclosed subword.Source: §3.1 · p. 8, §3.2 · p. 9
• Linear-path until expresses the global requirement that every write be followed by a read before another write, without using nesting edges.The specification is stated using wr and rd propositions and linear until.Source: §3.2 · p. 8
• CaRet's abstract-path operators express procedure total and partial correctness and can specify that the same procedure invocation later reads a variable before writing it again.Abstract paths skip invocations of procedures called from the current procedure.Source: §3.2 · pp. 8–9
• Call-since paths encode the active call stack for context-sensitive requirements, while a scope-bounded path ends when its procedure invocation returns.The section gives a requirement that procedure A be invoked only within procedure B's context, without an intervening call to overriding module C.Source: §3.2 · p. 9

4. Expressive Completeness

• NWTL remains FO-expressively complete when extended with other first-order-expressible operators, and the model-checking upper bounds are shown for NWTL+.Source: §4 · p. 10
• Adding a within operator suffices for expressive completeness in verification-style logics, confirming; in NWTL it preserves expressiveness but makes formulas exponentially more succinct.The operator evaluates a formula on a nested subword.Source: §4 · p. 10

4.1. Expressive completeness and NWTL.

• NWTL is expressively equivalent to FO over both finite and infinite nested words.The proof also establishes NWTLs = NWTLss = FO.Source: §4.1 · pp. 10, 12
• Every NWTL formula translates to an equivalent FO formula using at most three variables on finite and infinite nested words.Source: §4.1 · p. 10
• Every FO formula over nested words with at most one free variable is equivalent to an FO3 formula.Source: §4.1 · p. 16
• There are FO sentences over nested words that cannot be expressed in NWTLfuture.The passage’s example describes a first-position call whose matching return has a predecessor labeled a.Source: §4.1 · p. 17
• NWTL+, which adds all linear, call, and abstract until/since pairs, is expressively equivalent to FO over nested words.The future-only fragment of NWTL cannot express every FO sentence over nested words.Source: §4.1 · pp. 17–18

4.2. The within operator.

• LTLμ extended with the within operator W is expressively equivalent to FO over both finite and infinite nested words.At a call, W evaluates its formula on the subword through the matching return, or through the end of the word if the call is unmatched.Source: §4.2 · pp. 18–19

4.3. CaRet and other within operators.

• Adding within operators C and R to CaRet makes it expressively equivalent to FO over finite and infinite nested words.C evaluates on the interval from the innermost call to the current position; R evaluates from the current position through its corresponding return, or the word’s end when unmatched.Source: §4.3 · p. 20
• Every FO formula over finite or infinite nested words has an equivalent CaRet + {C, R} formula that does not use Ua.Source: §4.3 · p. 20
• Every CaRet + {R, C} formula translates recursively into an equivalent FO formula, with within operators handled by interval relativization.The translation relativizes FO quantifiers to the relevant interval.Source: §4.3 · p. 23
• Conversely, FO formulas are expressed in CaRet + {R, C} by induction on quantifier rank, using nested-word types and a composition method to encode existential witnesses.The construction characterizes types of composed words and uses them to express existential quantification.Source: §4.3 · pp. 24–26

5.1. Nested word automata.

• Nested-word automata propagate states along linear edges and hierarchical symbols along nesting edges, using both at matched returns.Source: §5.1 · p. 26

5.2. Tableau construction.

• The tableau tracks satisfied subformulas in automaton states and constructs a 2^O(|ϕ|)-size Büchi nested-word automaton for NWTL+.Source: §5.2 · pp. 27, 29

5. Model-Checking and Satisfiability

• NWTL+ satisfiability is EXPTIME-complete; model checking is polynomial in RSM or nested-word automaton size and exponential in formula size, also EXPTIME-complete.Source: §5 · p. 26, §5.2 · p. 29

5.3. Checking the within operator.

• Adding within makes NWTL+ satisfiability and Boolean-program model checking 2EXPTIME-complete, while yielding exponential gains in succinctness.Source: §5 · p. 26, §5.3 · p. 30

5.4. On within and succinctness.

• Within-extended formulas of size O(n) can require equivalent NWTL+ formulas of size 2^Ω(n), establishing exponential succinctness.Source: §5.4 · pp. 30–31

6.1. The three-variable property.

• Over finite or infinite nested words, every FO formula with at most two free variables is equivalent to an FO3 formula.The proof uses Ehrenfeucht–Fraïssé games; for the infinite case, it works through a forest representation of nested words.Source: §6.1 · p. 32

6.2. The two-variable fragment.

• Unary-NWTL captures FO2 using typed next operators and eventually operators over paths formed from nested-word edge types.The logic is defined over an FO2 vocabulary that includes successor relations and their transitive closures; the successor relations distinguish interior, call, return, call-return-summary, and call-interior-return-summary edges.Source: §6.2 · pp. 34–35
• An FO2 formula ϕ(x) translates to equivalent unary-NWTL of size 2^O(|ϕ|(qdp(ϕ)+1)) and operator depth at most 10 qdp(ϕ), with translation computable in polynomial time in the output size.The theorem states expressiveness equivalence and gives these translation bounds when formulas are viewed as DAGs with shared identical subformulas.Source: §6.2 · p. 35
• The translation bounds operator depth by 10 times quantifier depth and proves a DAG-size bound by induction on quantifier depth.Identical subformulas are shared when measuring formula size.Source: §6.2 · p. 37
• The translation to unary-NWTL can be computed in time polynomial in the size of its output formula.Source: §6.2 · p. 37
• Unary-NWTL model checking has the same complexity as NWTL model checking, using a variant of the tableaux construction.The construction is described as a variant of the tableaux method from Section 5.Source: §6.2 · p. 37

• The new temporal logics are first-order expressively complete.Source: §7 · p. 37
• First-order logic over nested words has the three-variable property, and a temporal logic is complete for its two-variable fragment.Source: §7 · p. 37
• NWTL+ satisfiability is EXPTIME-complete, while model checking is polynomial in RSM size and exponential in formula size.Source: §7 · p. 37
• Adding the within modality to NWTL makes model checking doubly exponential.Source: §7 · p. 37
• Whether CaRet is first-order complete remains open, though the authors conjecture that it is not.Source: §7 · p. 37

Appendix A. Proof of Lemma 4.3

• Correctness of the NWTLss-to-NWTL translation is proved by induction on formula structure, reducing the argument to until/since operators.Source: Appendix A · p. 39
• Conversely, the translated conditions yield a semi-strict path on which ψ holds before θ, establishing the until/since equivalence.Source: Appendix A · p. 39
• The proof translates a semi-strict path witnessing ψUσθ into summary-path conditions, handling cases based on matched calls and the path endpoint.Source: Appendix A · pp. 41–43