| || |
The informal semantics of the most interesting constructs are as follows:
- : if interval is non-empty then the value of in the next state of that interval
else an arbitrary value.
- : if interval is finite then the value of in the last state of that interval else
an arbitrary value.
- unit interval (length 1).
- holds if the interval can be decomposed (“chopped”) into a prefix and suffix
interval, such that holds over the prefix and over the suffix, or if the interval
is infinite and holds for that interval.
- holds if the interval is decomposable into a finite number of intervals such that
for each of them holds, or the interval is infinite and can be decomposed into an
infinite number of finite intervals for which holds.
Let be the “meaning” (semantic) function from to and let
be the “meaning” function from to (set of Boolean values,
) and let be an interval. We write if the intervals and are
identical with the possible exception of their mappings for the variable . The formal semantics
is listed in Table 2:
Table 2: Semantics of ITL