Question

w denotes a non-empty finite or infinite word over Σ. L0, L1 denote local variable contexts.

The rules defining neutral satisfaction of an assertion are identical to those without local variables, but with the

understanding that the underlying properties can have local variables.

Neutral satisfaction of properties:

? w Q iff w, {} Q.

? w, L0 Q iff w, L0 Q’, where Q’ is the unclocked property that results from Q by applying the rewrite

rules.

? w, L0 disable iff (b) P iff either w, L0 P or there exists 0 < k < |w| such that

w k b[L0] and w 0, k–1Tω, L0 P. Here, w 0, –1 denotes the empty word.

? w, L0 not P iff w, L0 P .

? w, L0 R iff there exist 0 < j < |w| and L1 such that w 0, j, L0, L1 R .

? w, L0 ( R |-> P ) iff for every 0 < j < |w| and L1 such that w 0, j, L0, L1 R, w j.., L1 P .

? w, L0 ( P ) iff w, L0 P.

? w, L0 ( P1 or P2 ) iff w, L0 P1 or w, L0 P2.

? w, L0 ( P1 and P2 ) iff w, L0 P1 and w, L0 P2.