時相演算子の意味論

Liloは、離散的な時間と連続的な時間の両方を取り扱うという意味で、やや非標準的な時相論理の意味論を採用しています。

Tを型とします。型Tのサンプルとは、{time : Real, value : T}というペアです。型Tの信号とは、時間値が狭義単調増加である型Tのサンプルが少なくとも2つ以上並んだ有限列です。Signal[T]を型Tの全ての信号の集合と記します。信号の最初のサンプルが時刻0である必要はありません。信号σが与えられたとき、σの要素をσ[0]、σ[1]、…、σ[n-1]と表記します（nはσのサンプル数）。σのサンプル数とσの持続時間（σ[n-1].time - σ[0].time）は区別することに注意してください。

信号σのサポート（support(σ)と表記）は、σのサンプルに紐づいた時間値の集合、すなわちsupport(σ) = {σ[i].time | 0 ≤ i < n}です。時刻tにおけるσの値をσ[time = t]と記します。すなわちσ[time = t] = σ[i].value（ここでiはσ[i].time = tとなるインデックス）。σ[time = t]はt ∈ support(σ)の場合にのみ定義されることに注意してください。

各Lilo式φは、Liloの型システムによって何らかの型Tを持つと判定されます（φ : Tと記します）。型TのLilo式の意味論は、Signal[S] → Signal[T]型の関数として理解されます（Sはシステムの入力信号の型）。この関数はサポートを保存、すなわち出力信号は入力信号と全く同じ時間値上で定義されます。型Tの式φに対して、〚φ〛でこの関数を表します。

非時相演算子には、標準的なブール演算子、算術演算子、比較演算子、条件分岐などが含まれます。ある式がポイントワイズな式であるとは、任意の固定時間値tに対して、出力信号〚φ〛(σ)[time = t]の値が入力信号の値σ[time = t]のみに依存することをいいます。Lilo式が非時相的であるとは、その解釈が入力信号に依存しないことをいいます。したがって、ポイントワイズな式は入力信号と非時相演算子から構成され、非時相式はパラメータ、定数、および非時相演算子から構成されます。

実数の区間は[a, b]というペアで書きます（a: Real、b: Real | infinity、a ≤ b）。bがinfinityである場合、その区間は非有界であるといい、そうでない場合は有界であるといいます。時間点tと区間Iに対して、t + Iまたはt - Iでそれぞれ{t + x | x ∈ I}または{t - x | x ∈ I}を表します。各時相演算子がサポートを保存するため、このドキュメントではt + Iおよびt - Iを(t + I) ∩ support(σ)および(t - I) ∩ support(σ)の省略形として使います。

Liloの時相演算子は、一部の例外を除いて区間で注釈されます。φ : Boolが与えられたとき、以下の時相演算子を定義します。

• Always: 〚always[I] φ〛(σ)[time = t] = trueは、全てのt' ∈ (t + I)に対して〚φ〛(σ)[time = t'] = trueであるとき、かつそのときに限り成立します。
• Eventually: 〚eventually[I] φ〛(σ)[time = t] = trueは、〚φ〛(σ)[time = t'] = trueとなるt' ∈ (t + I)が存在するとき、かつそのときに限り成立します。
• Historically: 〚historically[I] φ〛(σ)[time = t] = trueは、全てのt' ∈ (t - I)に対して〚φ〛(σ)[time = t'] = trueであるとき、かつそのときに限り成立します。
• Past: 〚past[I] φ〛(σ)[time = t] = trueは、〚φ〛(σ)[time = t'] = trueとなるt' ∈ (t - I)が存在するとき、かつそのときに限り成立します。
• Until: 〚φ until[I] ψ〛(σ)[time = t] = trueは、〚ψ〛(σ)[time = t'] = trueとなるt' ∈ (t + I)が存在し、かつt ≤ t'' < t'を満たす全てのt'' ∈ support(σ)に対して〚φ〛(σ)[time = t''] = trueであるとき、かつそのときに限り成立します。
• Since: 〚φ since[I] ψ〛(σ)[time = t] = trueは、〚ψ〛(σ)[time = t'] = trueとなるt' ∈ (t - I)が存在し、かつt' < t'' ≤ tを満たす全てのt'' ∈ support(σ)に対して〚φ〛(σ)[time = t''] = trueであるとき、かつそのときに限り成立します。

alwaysとeventuallyは互いに論理的双対であることに注意してください。untilの論理的双対はreleasesであり、φ releases[I] ψは!(!φ until[I] !ψ)として定義されます。演算子since、historically、pastはそれぞれuntil、always、eventuallyの過去時相版です。

will_changeとdid_changeは、等号が定義されている任意の型（現在は関数型でない型）φ : Tに対して次のように定義されます。

• Will Change: 〚will_change[I] φ〛(σ)[time = t] = trueは、〚φ〛(σ)[time = t'] ≠ 〚φ〛(σ)[time = t'']となる2点t', t'' ∈ (t + I)が存在するとき、かつそのときに限り成立します。
• Did Change: 〚did_change[I] φ〛(σ)[time = t] = trueは、〚φ〛(σ)[time = t'] ≠ 〚φ〛(σ)[time = t'']となる2点t', t'' ∈ (t - I)が存在するとき、かつそのときに限り成立します。

以下の演算子には区間を付けることができません。また重要なこととして、これらは離散時間意味論で定義されます。すなわち、関連付けられたtimeではなく、サンプルに関連付けられた離散的なインデックスに依存します。式φの型がTであり、vが型Tの非時相的な値である場合、式next φ、previous φ、next_with v φ、previous_with v φも同様に型Tを持ちます。nを入力信号σのサンプル数とします。

• Next: 0 ≤ i < n - 1に対して〚next φ〛(σ)[i] = 〚φ〛(σ)[i + 1]、〚next φ〛(σ)[n - 1] = 〚φ〛(σ)[n - 1]。
• Previous: 0 < i < nに対して〚previous φ〛(σ)[i] = 〚φ〛(σ)[i - 1]、〚previous φ〛(σ)[0] = 〚φ〛(σ)[0]。
• Next With: 0 ≤ i < n - 1に対して〚next_with v φ〛(σ)[i] = 〚φ〛(σ)[i + 1]、〚next_with v φ〛(σ)[n - 1] = v。
• Previous With: 0 < i < nに対して〚previous_with v φ〛(σ)[i] = 〚φ〛(σ)[i - 1]、〚previous_with v φ〛(σ)[0] = v。

以下のスライディングウィンドウ演算子は、値が数値型である任意の式φに対して定義されます。また、関連する区間は[0, b]の形式（bは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}。