時相論理 (temporal logic)
ある条件が最終的に真となるとか、別の事実が真になるまでその条件は真であるとかいった将来の出来事について論理式で表す
時相論理演算子
| 演算子 | 読み方 | 意味 |
|---|---|---|
| [] P | Always | 状態列において、常に P であること。 |
| <> P | Eventually | 状態列において、いつかは P であること。 |
[]<>と<>[]について
- []<>Pは、PがFALSEになることがあってもいつかまたTRUEになる(無限回trueになる)
- <>[]Pは、PにあるTRUE状態以降にFALSEに一度もならないようなTRUEが存在する
- すべてのプロセスがいつかは完了するということは以下のように定義できる。
Termination == <>(\A self \in ProcSet: pc[self] = "Done)
P~>Q （P leads to Q）
PとなればQという結果になる。Pという状態列において、TRUEになる状態があれば、Qがその状態またはそれ以降の状態においてTRUEになる。
スタッターステップ (stuttering step)
2 つ以上の独立した状態変数で構成されるシステムではある値が変化したときに別の値が変化しているとは限らない。
このようなシステムでは特定の状態変数に対して変化しないステップを仕様として許可する必要がある (このような状態変数が変化しないステップをスタッターステップ (stuttering step) と呼ぶ)。たとえば時刻と温度を示す変数が２つあるとき、時計だけが変化するが温度は変化しない、または時計は変化せず、温度だけが変化する。これを許可する必要がある。
スターターステップを許容する問題としてある状態のままであり続けるという点がある。例えば温度が変化するが時刻は変化しない。永遠に時計が止まり続ける。といった問題がある。スタッターステップを取り除くには公平性を追加する。
このようなシステムでは特定の状態変数に対して変化しないステップを仕様として許可する必要がある (このような状態変数が変化しないステップをスタッターステップ (stuttering step) と呼ぶ)。たとえば時刻と温度を示す変数が２つあるとき、時計だけが変化するが温度は変化しない、または時計は変化せず、温度だけが変化する。これを許可する必要がある。
スターターステップを許容する問題としてある状態のままであり続けるという点がある。例えば温度が変化するが時刻は変化しない。永遠に時計が止まり続ける。といった問題がある。スタッターステップを取り除くには公平性を追加する。
公平性
公平性に関する記述がない場合、制御対象のステップが進行可能だったとしても、永遠にスタッターリングを繰り返して進行しない可能性がある (任意の位置で Crash-Stop する)。
弱い公平性
ステップが進行可能な条件が継続して続くのであればいつか進行する公平性を弱い公平性 (weak fairness)と呼ぶ。fairと記述する。
強い公平性
進行可能と進行不可能が断続的に繰り返されたとしてもいつか進行する公平性を強い公平性 (strong fairness) と呼ぶ。fair+と記述する。
公平性の記述
公平性を指定する fair (弱い公平性) または fair+ (強い公平性) キーワードは algorithm の前か process の前に付与することができる。また Step:+ のように個別のステップのラベルのあとに + または - を付加してそのステップのみ公平性を変更することもできる。
公平性特性を付与してよいのはモデル検査で対象とするシステムを構成するプロセス、つまりプロセスの一つでも Crash-Stop したらそもそもサービスや機能を続行することができないような、システムの主旨たるプロセスに限られる。Crash-Stop 障害を想定する必要のある外部のサブシステム役となるプロセスには公平性特性を付与してはならない。
公平性特性を付与してよいのはモデル検査で対象とするシステムを構成するプロセス、つまりプロセスの一つでも Crash-Stop したらそもそもサービスや機能を続行することができないような、システムの主旨たるプロセスに限られる。Crash-Stop 障害を想定する必要のある外部のサブシステム役となるプロセスには公平性特性を付与してはならない。
WF_vars(A) と SF_vars(A) という記法があらかじめ用意されている。
[Amazon商品]
