Semantics of Temporal Operators

Lilo adopts a semantics for temporal logic that is slightly non-standard, in the sense that it takes into account both a discrete and a continuous notion of time.

Background

Let T be a type. A sample of type T is a pair {time : Real, value : T}. A signal of type T is a finite sequence of at-least two samples of type T such that the time values are strictly increasing. We write Signal[T] to be the set of all signals of type T. We do not require the first sample of a signal to be at time 0. Given a signal σ, we denote the elements of σ as σ[0], σ[1], …, σ[n-1] where n is the number of samples of σ. Note that we distinguish between the number of samples of σ and the duration of σ (which is σ[n-1].time - σ[0].time).

The support of a signal σ, denoted support(σ), is the set of time values associated with the samples of σ, i.e., support(σ) = {σ[i].time | 0 ≤ i < n}. Two different notations are used to index samples in signals. We write σ[time = t] to denote the value of σ at time t, i.e., σ[time = t] = σ[i].value where i is such that σ[i].time = t. Note that σ[time = t] is only defined for t ∈ support(σ).

Consider, for example, the signals v : Int and b : Bool defined by the following samples:

v = [{time: 1.0, value: 10}, {time: 3.0, value: 20}, {time: 4.0, value: 20}, {time: 5.0, value: 30}, {time: 7.5, value: 40}, {time: 10.0, value: 20}, {time: 11.0, value: 10}, {time: 12.0, value: 10}]
b = [{time: 1.0, value: true}, {time: 3.0, value: false}, {time: 4.0, value: false}, {time: 5.0, value: true}, {time: 7.5, value: false}, {time: 10.0, value: true}, {time: 11.0, value: true}, {time: 12.0, value: true}]

They can be visualized as follows

Both v and b have 8 samples numbered from 0 to 7. The support of both signals is {1.0, 3.0, 4.0, 5.0, 7.5, 10.0, 11.0, 12.0}. The same sample with value 30 can be indexed as v[time = 5.0] or v[3].

Each Lilo formula φ is judged to be of some type T (written φ : T), by the Lilo type system. The semantics of a Lilo formula of type T is understood as a function of type Signal[S] → Signal[T], where S is the type of the input signals described by the system. This function is defined to be support-preserving, i.e., the output signal is defined on exactly the same time values as the input signal. For a formula φ of type T, we write 〚φ〛 to denote this function.

Atemporal operators include the standard Boolean operators, arithmetic operators, comparison operators, conditionals and so on. A formula is said to be a pointwise formula if for any fixed time value t, the value of the output signal 〚φ〛(σ)[time = t] depends only on the value of the input signal σ[time = t]. A lilo expression is said to be atemporal if its intepretation does not depend on the input signals, and are therefore constant over time. Thus, a pointwise formula is built from input signals and atemporal operators, and an atemporal expression is built from params, constants and atemporal operators.

Consider the following lilo system

system main

signal v : Int
signal b : Bool
param p : Int

Here, the formula v * 2 is pointwise, while the formula p * 2 is atemporal. The formula eventually [0, 5] (v > p) is neither pointwise nor atemporal.

An interval of real numbers is written as a pair [a, b] where a: Real and b: Real | infinity with 0 ≤ a ≤ b. If b is infinity, we say that the interval is unbounded, and otherwise we say that the interval is bounded. For a time point t and an interval I, we write t + I or t - I to denote {t + x | x ∈ I} or {t - x | x ∈ I} respectively.

Note that the intervals t + I or t - I may be completely or partially outside the support of the input signal, possibly overshooting its upper and lower bounds. However, since our temporal operators are support-preserving, and are defined in terms of the intersection of these intervals with the support, this is of no consequence.

Temporal Operators and their Semantics

Temporal operators in Lilo, with some exceptions, are annotated with an interval. Given φ : Bool, we define the following temporal operators.

• Always: 〚always[I] φ〛(σ)[time = t] = true, if for all t' ∈ (t + I) ∩ support(σ), 〚φ〛(σ)[time = t'] = true.
• Eventually: 〚eventually[I] φ〛(σ)[time = t] = true, if there exists t' ∈ (t + I) ∩ support(σ) such that 〚φ〛(σ)[time = t'] = true.
• Historically: 〚historically[I] φ〛(σ)[time = t] = true, if for all t' ∈ (t - I) ∩ support(σ), 〚φ〛(σ)[time = t'] = true.
• Past: 〚past[I] φ〛(σ)[time = t] = true, if there exists t' ∈ (t - I) ∩ support(σ) such that 〚φ〛(σ)[time = t'] = true.
• Until: 〚φ until[I] ψ〛(σ)[time = t] = true, if there exists t' ∈ (t + I) ∩ support(σ) such that 〚ψ〛(σ)[time = t'] = true and for all t'' ∈ support(σ) satisfying t ≤ t'' < t', 〚φ〛(σ)[time = t''] = true.
• Since: 〚φ since[I] ψ〛(σ)[time = t] = true, if there exists t' ∈ (t - I) ∩ support(σ) such that 〚ψ〛(σ)[time = t'] = true and for all t'' ∈ support(σ) satisfying t' < t'' ≤ t, 〚φ〛(σ)[time = t''] = true.

Considering the signal b from the running example, the formulas always [1,2] b and eventually [1,2] b evaluate to the following. The formula (v >= 20) until [1, 2] b evaluates to the following.

Note that the always and eventually operators are logical duals of each other. The logical dual of until is releases, i.e., φ releases[I] ψ is defined as !(!φ until[I] !ψ). The operators since, historically and past are the past-time counterparts of until, always and eventually respectively.

The operators will_change and did_change are defined for any well-typed φ : T for which equality is defined (all non-function types, in practice) as follows.

• Will Change: 〚will_change[I] φ〛(σ)[time = t] = true, if there exist two points t', t'' ∈ (t + I) ∩ support(σ) such that 〚φ〛(σ)[time = t'] ≠ 〚φ〛(σ)[time = t''].
• Did Change: 〚did_change[I] φ〛(σ)[time = t] = true, if there exist two points t', t'' ∈ (t - I) ∩ support(σ) such that 〚φ〛(σ)[time = t'] ≠ 〚φ〛(σ)[time = t''].

The following operators cannot be annotated with an interval. And importantly, they are defined on the discrete time-semantics, i.e., they depend on the discrete index associated with the samples rather than the associated time. If the base formula φ is of type T, then so are the formulas next φ and previous φ. We write n to denote the number of samples of the input signal σ.

• Next: 〚next φ〛(σ)[i] = 〚φ〛(σ)[i + 1] for 0 ≤ i < n - 1 and 〚next φ〛(σ)[n - 1] = 〚φ〛(σ)[n - 1].
• Previous: 〚previous φ〛(σ)[i] = 〚φ〛(σ)[i - 1] for 0 < i < n and 〚previous φ〛(σ)[0] = 〚φ〛(σ)[0].

The following sliding window operators are defined for any φ whose value is a numeric type. Note also that the associated interval must be of the form [0, b] where b is possibly infinity.

• Future Maximum: 〚max_future [0, a] φ〛(σ)[time = t] = max{〚φ〛(σ)[time = t'] | t' ∈ support(σ), t ≤ t' ≤ t + a}.
• Past Maximum: 〚max_past [0, a] φ〛(σ)[time = t] = max{〚φ〛(σ)[time = t'] | t' ∈ support(σ), t - a ≤ t' ≤ t}.
• Future Minimum: 〚min_future [0, a] φ〛(σ)[time = t] = min{〚φ〛(σ)[time = t'] | t' ∈ support(σ), t ≤ t' ≤ t + a}.
• Past Minimum: 〚min_past [0, a] φ〛(σ)[time = t] = min{〚φ〛(σ)[time = t'] | t' ∈ support(σ), t - a ≤ t' ≤ t}.

Behavior of Temporal Operators at Signal Boundaries

At some time = t, the interval t + I or t - I may be completely or partially outside the support of the input signal σ. We clarify the behavior of the temporal operators in such cases.

• Eventually, Past: For eventually[I] φ or past[I] φ to be true, a witness of φ being true must exist. Specifically, if (t + I) ∩ support(σ) = ∅ or (t - I) ∩ support(σ) = ∅, then 〚eventually[I] φ〛(σ)[time = t] = false and 〚past[I] φ〛(σ)[time = t] = false.
• Always, Historically: The formulas always[I] φ or historically[I] φ are determined by the truth of φ everywhere in our intersection of interest with the support. When empty, the formulas are vacuously true. Formally, if (t + I) ∩ support(σ) = ∅ or (t - I) ∩ support(σ) = ∅, then 〚always[I] φ〛(σ)[time = t] = true and 〚historically[I] φ〛(σ)[time = t] = true.
• Until, Since: In the case of the formulas φ until[I] ψ or φ since[I] ψ, the witness for ψ must exist. If (t + I) ∩ support(σ) = ∅ or (t - I) ∩ support(σ) = ∅, then 〚φ until[I] ψ〛(σ)[time = t] = false and 〚φ since[I] ψ〛(σ)[time = t] = false. On the other hand, if there are no time points in support(σ) between t and the witness for ψ, then the formula does not require the truth of φ anywhere.
• Next, Previous: The values of next φ and previous φ are defined by the closest sample in the direction of interest. We have 〚previous φ〛(σ)[0] = 〚φ〛(σ)[0]. If the signal has n samples, then the last sample satisfies 〚next φ〛(σ)[n - 1] = 〚φ〛(σ)[n - 1].
• Will Change, Did Change: The formulas will_change[I] φ and did_change[I] φ require two distinct time points in the intersection of interest with the support. If (t + I) ∩ support(σ) or (t - I) ∩ support(σ) has only one time point or no time points, then 〚will_change[I] φ〛(σ)[time = t] = false and 〚did_change[I] φ〛(σ)[time = t] = false.
• Maximum, Minimum: The intervals allowed in the formulas {max,min}_{future,past} are required to begin with 0. Therefore, if t ∈ support(σ), then t also satisfies t ∈ ((t + I) ∩ support(σ)), and hence it cannot be empty. If this set is a singleton, the formula evaluates to the value of φ at the time t itself.

Consider the values of the formulas always [1, 2] b and eventually [1, 2] b in the illustration above. At times t = 5, 7.5, and 12, the intervals t + [1, 2] are [6, 7], [8.5, 9.5], and [13, 14] respectively. The intersection of these intervals with the support of b is empty, as shown in the timeline below. Thus, no witness for eventually exists, and the formula eventually [1, 2] b evaluates to false on all of these points. On the other hand, the formula always [1, 2] b evaluates to true on all of these points, since it is vacuously true (i.e., there are no points in the support of b on which the formula imposes a constraint).

Similarly, in the formula (v >= 20) until [1, 2] b, at times t = 5, t = 7.5 and t = 12, the formula evaluates to false since there is no witness for b in the intervals of interest.