Personal tools
You are here: Home LTS LTSA チュートリアル 第三回 Parallel Composition
Document Actions

Parallel Composition

by takeuchi last modified 2008-11-23 19:26

Parallel Composition(並列合成) についての説明です.action のインターリーブです.

定義

P と Q がプロセスならば,(P||Q) は P と Q の並列実行を表します."||"は並列結合演算子といいます.

  • 交換則: (P||Q) = (Q||P).
  • 結合則: (P||(Q||R)) = ((P||Q)||R) = (P||Q||R).

サンプル

ITCH  = (scratch->STOP).
CONVERSE = (think->talk->STOP).
||CONVERSE_ITCH = (ITCH || CONVERSE).

composite process の遷移は次のようになります.action をインターリーブした結果の軌跡です.

think -> talk -> scratch
think -> scratch -> talk
scratch -> think -> talk

LTS は以下のようになる.ITCH と CONVERSE を組み合わせると CONVERSE_ITCH となる.action がインタリーブしていることがわかる.

converse

LTSA では,上のボタンを押すと並列合成された LTS 図が出力される.