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.

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}. 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(σ).

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 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. Thus, a pointwise formula is built from input signals and atemporal operators, and an atemporal expression is built from params, constants and atemporal operators.

An interval of real numbers is written as a pair [a, b] where a: Real and b: Real | infinity with 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. In our case, since each of the temporal operators preserves support, we will write t + I and t - I as a shorthand for (t + I) ∩ support(σ) and (t - I) ∩ support(σ).

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

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 (which is currently all non-function types) as follows.

• Will Change: 〚will_change[I] φ〛(σ)[time = t] = true if and only if there exists two points t', t'' ∈ (t + I) such that 〚φ〛(σ)[time = t'] ≠ 〚φ〛(σ)[time = t''].
• Did Change: 〚did_change[I] φ〛(σ)[time = t] = true if and only if there exists two points t', t'' ∈ (t - I) 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, and v is an atemporal value of type T, then so are the formulas next φ, previous φ, next_with v φ and previous_with v φ. 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].
• Next With: 〚next_with v φ〛(σ)[i] = 〚φ〛(σ)[i + 1] for 0 ≤ i < n - 1 and 〚next_with v φ〛(σ)[n - 1] = v.
• Previous With: 〚previous_with v φ〛(σ)[i] = 〚φ〛(σ)[i - 1] for 0 < i < n and 〚previous_with v φ〛(σ)[0] = v.

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}.