Software Engineering Lecture s08-2
Menu Menu
状態遷移図を作るには...
状態遷移は、イベントと状態の名前の集合を決めることから始まる。まず、状態遷移の切っ掛けになるものを探す。
電子レンジのスイッチ
電子レンジのタイマー
これ自体はイベントではないことに注意しよう。
電子レンジのスイッチをオンにする
電子レンジのスイッチをオフにする
電子レンジのタイマーを10にセット
電子レンジのタイマーが0になる
などが状態遷移の条件となる。これらは、同時あるいは排他的に起きるイベントとなる。これらに何か名前を付けよう。
電子レンジのスイッチをオンにする son
電子レンジのスイッチをオフにする soff
電子レンジのタイマーを10にセット t_10
電子レンジのタイマーが0になる t_off
変数があると、それがそのまま状態遷移を増やしてしまう。
状態は、まず、初期状態がある。
電子レンジのスイッチが切れていて、ドアが閉まっている
これに、s0という名前を付ける。
s0 から、起きる可能性のある全てのイベントを列挙する。それが異なる状態を作るならば、それは新しい名前を持つ状態である。
s0 --son--> s1 (電子レンジのスイッチがon)
s0 --sooff--> s0 (そのまま)
s0 --t_10--> s0 (そのまま)
x s0 --t_off--> s0 禁止
新しい状態 s1 に対して、起きる可能性のある全てのイベントを列挙する。それが異なる状態を作る。
これを生成された状態に対して、同じ状態が生成されなくなるまで繰り返す。
SPIN で状態を表す
spin は、 モデル検証ツール であり、状態遷移系を表現する特別な言語を持っている。
時相論理
この状態遷移がどういう性質を満たしているかは、
ドアが開いている時は、電子レンジがオンにならない
などの表現で表される。これは、通常の論理とは別に時間の概念を含んでいる。
□(p) いつも p
◇(p) いつか p
p & q p の後に、q が起きる
p U q q が起きるまで、ずーっと p
などの様相演算子と呼ばれるものを論理に付け加えることで論理を時間に対して拡張することが出来る。時間論理にはいろんなものがあり、特に状態遷移に着目した論理を時相論理と呼ぶ。
Interval Temporal Logic
ITLは時区間によって論理式の真理値が異なる論理である。この論理の意味論(Semantics)の定義には、M(P) meaning fucntion を使う。これによって式の論理値を決めることができる。σ0は時刻を表し、σ0...σnは時区間を表す。
| Mσ0σ1...σn(p) | = | T/F (p は命題変数) 通常はさらに M σ0...σn(p) = M σ0(p) を要求する (変数は時刻にのみ依存する(Locality)) |
| M σ0σ1...σn(P&Q) | = | 0≦∃i≦n∧ M σ0...σi(P)∧ M σi...σn(Q), (P,Q は、任意の式) |
| M σ0σ1...σn(@ P) | = | Mσ1...σn(P) (もしn=0だったF) |
| M σ0σ...σn(empty) | = | T iff n=0 |
| Mσ0σ1...σn(*P) | = | ∃i, 0≦i≦n, Mσ0...σi(P) ∧ (M σi...σn(*P ∨ empty)), |
| その他、普通の論理の記号(¬,∧,⇒,⇔)を使う。例えば | ||
| Mσ0σ1...σn(P ∧ Q) | = | Mσ0...σn(P) ∧ Mσ0...σn(Q) |
例題
- ◇P ≡ T & P
- □P ≡ ~◇~P
- more ≡ ~ empty
- ○P ≡ @P ∨ empty
- fin(P) ≡T & (P ∧ empty)
- keep(P) ≡□P & @empty
- ◇□P ⇔ □◇P ⇔ fin(P)
Tableau expansion of ITL
このtableau methodでは、式を現在時刻と未来の時刻に分割する| T | → | empty∧ T |
| more ∧ @T | ||
| P&Q | → | empty∧ P∧Q |
| (more ∧ more(P)&Q) ∨ ((empty(P)∧empty)&Q) | ||
| @P | → | empty∧ F |
| more ∧ P |
Disjunction を決定的に展開する。それにより、tableu全体を決定的に展開することができる。こうしないと、否定を計算する際に、一旦、tableau のdisjuctive normal formを再計算する必要がある。