Document Actions
LTS とは
LTS と FSP についての説明をしています．
LTS (Labeled Transition System)
以下の形式で描かれた状態機械をLTS (ラベル付き遷移システム) といいます．
- 初期状態は0と番号付け
- 遷移は時計回りに描画
- 遷移に action name をラベル付け
LTS のサンプル画像
on と off を繰り返すスイッチの LTS は以下のようになります．
FSP (Finite State Process)
LTS を代数的に表現するための言語．
- action は小文字，process は大文字
FSP のサンプル
on と off を繰り返すスイッチの FSP は以下のようになります．
SWITCH = OFF,
OFF = (on -> ON),
ON = (off-> OFF).