定義

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 がインタリーブしていることがわかる．

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