時相演算子の意味論

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}です。信号のサンプルにインデックスを付けるため、2つの異なる記法を使用します。時刻tにおけるσの値をσ[time = t]と記します。すなわちσ[time = t] = σ[i].value（ここでiはσ[i].time = tとなるインデックス）。σ[time = t]はt ∈ support(σ)の場合にのみ定義されることに注意してください。

例として、次のサンプルによって定義される信号v : Intとb : Boolを考えます：

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

これらは次のように可視化できます。

vとbにはどちらも0から7までの番号が付いた8つのサンプルがあります。両方の信号のサポートは{1.0, 3.0, 4.0, 5.0, 7.5, 10.0, 11.0, 12.0}です。値30を持つ同じサンプルをv[time = 5.0]またはv[3]として参照できます。

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

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

次のLiloシステムを考えます。

system main

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

ここで、式v * 2はポイントワイズであり、式p * 2は非時相的です。式eventually [0, 5] (v > p)はポイントワイズでも非時相的でもありません。

実数の区間は[a, b]というペアで書きます（a: Real、b: Real | infinity、0 ≤ a ≤ b）。bがinfinityである場合、その区間は非有界であるといい、そうでない場合は有界であるといいます。時間点tと区間Iに対して、t + Iまたはt - Iでそれぞれ{t + x | x ∈ I}または{t - x | x ∈ I}を表します。

区間t + Iまたはt - Iは、入力信号のサポートから完全または部分的に外れ、その上限や下限を超える場合があります。しかし、時相演算子はサポートを保存し、これらの区間とサポートとの共通部分を使って定義されるため、問題にはなりません。

時相演算子とその意味論

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

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

上記の例の信号bについて、式always [1,2] bとeventually [1,2] bは次のように評価されます。 式(v >= 20) until [1, 2] bは次のように評価されます。

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

will_changeとdid_changeは、等号が定義されている任意の適切に型付けされたφ : T（実際には、すべての非関数型）に対して次のように定義されます。

• Will Change: 〚φ〛(σ)[time = t'] ≠ 〚φ〛(σ)[time = t'']となる2点t', t'' ∈ (t + I) ∩ support(σ)が存在する場合、〚will_change[I] φ〛(σ)[time = t] = trueです。
• Did Change: 〚φ〛(σ)[time = t'] ≠ 〚φ〛(σ)[time = t'']となる2点t', t'' ∈ (t - I) ∩ support(σ)が存在する場合、〚did_change[I] φ〛(σ)[time = t] = trueです。

以下の演算子には区間を付けることができません。また重要なこととして、これらは離散時間意味論で定義されます。すなわち、関連付けられたtimeではなく、サンプルに関連付けられた離散的なインデックスに依存します。基本となる式φの型がTである場合、式next φ、previous φも同様に型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]。

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

信号の境界における時相演算子の動作

あるtime = tにおいて、区間t + Iまたはt - Iが入力信号σのサポートから完全または部分的に外れることがあります。このような場合の時相演算子の動作を明確にします。

• Eventually、Past: eventually[I] φまたはpast[I] φが真になるには、φが真となる証拠が存在しなければなりません。具体的には、(t + I) ∩ support(σ) = ∅または(t - I) ∩ support(σ) = ∅の場合、〚eventually[I] φ〛(σ)[time = t] = falseおよび〚past[I] φ〛(σ)[time = t] = falseです。
• Always、Historically: 式always[I] φまたはhistorically[I] φは、対象となる区間とサポートとの共通部分のすべての点におけるφの真偽によって決まります。この共通部分が空の場合、式は空虚に真となります。形式的には、(t + I) ∩ support(σ) = ∅または(t - I) ∩ support(σ) = ∅の場合、〚always[I] φ〛(σ)[time = t] = trueおよび〚historically[I] φ〛(σ)[time = t] = trueです。
• Until、Since: 式φ until[I] ψまたはφ since[I] ψの場合、ψの証拠が存在しなければなりません。(t + I) ∩ support(σ) = ∅または(t - I) ∩ support(σ) = ∅の場合、〚φ until[I] ψ〛(σ)[time = t] = falseおよび〚φ since[I] ψ〛(σ)[time = t] = falseです。一方、tとψの証拠との間にsupport(σ)の時間点が存在しない場合、式はどの点でもφが真であることを要求しません。
• Next、Previous: next φとprevious φの値は、対象となる方向で最も近いサンプルによって定義されます。〚previous φ〛(σ)[0] = 〚φ〛(σ)[0]です。信号にn個のサンプルがある場合、最後のサンプルについて〚next φ〛(σ)[n - 1] = 〚φ〛(σ)[n - 1]が成り立ちます。
• Will Change、Did Change: 式will_change[I] φとdid_change[I] φは、対象となる区間とサポートとの共通部分に2つの異なる時間点があることを要求します。(t + I) ∩ support(σ)または(t - I) ∩ support(σ)に時間点が1つしかない、あるいはまったくない場合、〚will_change[I] φ〛(σ)[time = t] = falseおよび〚did_change[I] φ〛(σ)[time = t] = falseです。
• Maximum、Minimum: 式{max,min}_{future,past}で許可される区間は0から始まる必要があります。したがって、t ∈ support(σ)であればt ∈ ((t + I) ∩ support(σ))も成り立つため、この集合が空になることはありません。この集合が単集合の場合、式は時刻t自体におけるφの値に評価されます。

上図の式always [1, 2] bとeventually [1, 2] bの値を考えます。時刻t = 5、7.5、12では、区間t + [1, 2]はそれぞれ[6, 7]、[8.5, 9.5]、[13, 14]です。下のタイムラインに示すように、これらの区間とbのサポートとの共通部分は空です。したがってeventuallyの証拠は存在せず、式eventually [1, 2] bはこれらすべての点でfalseに評価されます。一方、式always [1, 2] bは空虚に真となるため、これらすべての点でtrueに評価されます（つまり、この式が制約を課すbのサポート上の点がありません）。

同様に、式(v >= 20) until [1, 2] bは、時刻t = 5、t = 7.5、t = 12において、対象となる区間内にbの証拠がないためfalseに評価されます。