Question

Let P be the set of atomic propositions.

The semantics of assertions and properties is defined via a relation of satisfaction by empty, finite, and infinite

words over the alphabet Σ = 2P U {T, ⊥}. Such a word is an empty, finite, or infinite sequence of elements of Σ.

The number of elements in the sequence is called the length of the word, and the length of word w is denoted

|w|. Note that |w| is either a non-negative integer or infinity.

The sequence elements of a word are called its letters and are assumed to be indexed consecutively beginning

at zero. If |w| > 0, then the first letter of w is denoted w0; if |w| > 1, then the second letter of w is denoted w1; and

so forth. w i.. denotes the word obtained from w by deleting its first i letters. If i < |w|, then w i.. = w iw i+1.... If

i > |w|, then w i.. is empty.

If i < j, then w i, j denotes the finite word obtained from w by deleting its first i letters and also deleting all letters

after its ( j + 1)st. If i < j < |w|, then w i, j = w iw i+1...w j.

If w is a word over Σ, define w to be the word obtained from w by interchanging T with ⊥. More precisely,

w i = T if w i = ⊥ ; w i = ⊥ if w i = T; and w i = w i if w i is an element in 2P.

The semantics of clocked sequences and properties is defined in terms of the semantics of unclocked

sequences and properties. See the subsection on rewrite rules for clocks below.

It is assumed that the satisfaction relation ζ b is defined for elements ζ in 2P and boolean expressions b. For

any boolean expression b, define

T b and ⊥ b .