これまでの演算子を使った例である．p, q はもちろん状態を含んだ式になる． p → ◇ q 最初 p が真ならば，いつかは q が真になる． □ ( p → ◇ q) 先の例に対して，「以後」演算子がついている．t=0 […]
-
Pages
-
Categories
-
Archives
Category Archives: KAOS
KAOS (92) 過程ベースの仕様 (4.4.2-4)
11/11/2014 – 7:29 AM
演算子の続きである． 「以後(henceforth)」演算子 □ (σ, j) ⊧ □p iff (σ, k) ⊧ p for all k ≥ j. これといった訳語がない．「ずっと p である」といった意味にな […]
KAOS (91) 過程ベースの仕様 (4.4.2-3)
10/11/2014 – 8:13 AM
時相論理には，様々なタイプがある．時間を離散的と捉えるか・連続的と捉えるか．未来のみを扱うか・過去も扱うか．時間の分岐（可能な未来）をモデル化するか否か． ここでは，要求に関連しそうな基本的なところのみを扱う．また，ここ […]