時相論理 – risk = nil;

Tag Archives: 時相論理

KAOS (94) 過程ベースの仕様 (4.4.2-6)

13/11/2014 – 2:09 PM

今回は，過去を示す演算子である．引き続き教科書[ref]Pnueli, Amir, and Zohar Manna. “The temporal logic of reactive and concurren […]

By nil | Posted in KAOS, 形式仕様記述, 要求, 要求工学 | コメントを受け付けていません

KAOS (93) 過程ベースの仕様 (4.4.2-5)

12/11/2014 – 7:52 AM

これまでの演算子を使った例である．p, q はもちろん状態を含んだ式になる． p → ◇ q 最初 p が真ならば，いつかは q が真になる． □ ( p → ◇ q) 先の例に対して，「以後」演算子がついている．t=0 […]

By nil | Posted in KAOS, 形式仕様記述, 要求, 要求工学 | コメントを受け付けていません

KAOS (92) 過程ベースの仕様 (4.4.2-4)

11/11/2014 – 7:29 AM

演算子の続きである．「以後(henceforth)」演算子 □ (σ, j) ⊧ □p iff (σ, k) ⊧ p for all k ≥ j. これといった訳語がない．「ずっと p である」といった意味にな […]

By nil | Posted in KAOS, 形式仕様記述, 要求, 要求工学 | コメントを受け付けていません