スタッターバイシミュレーション

理論計算機科学において、スタッター双模倣とは、計算をモデル化する抽象機械である2つの遷移システム間の関係である。これは共帰納的に定義され、双模倣の考え方を一般化する。双模倣は、遷移が対応するように機械の状態を一致させる。スタッター双模倣は、遷移を有限パスフラグメントに一致させることを可能にする。^[1]

『モデル検査の原理』で、Baier と Katoen は単一の遷移システムに対するスタッター双模倣を定義し、後にそれを 2 つの遷移システム上の関係に適用します。 に対するスタッター双模倣は、R内のすべての ( s ₁、s ₂ )に対して次の式が成り立つようなS上の2 項関係Rです。 ${\displaystyle {\text{TS}}=(S,{\text{Act}},\to ,I,{\text{AP}},L)}$

1. ${\displaystyle s_{1},s_{2}}$同じラベルを持つ
2. が有効な遷移である場合、各ペアがRにあり、がRにあるような有限パスフラグメント（ ）が存在する。${\displaystyle s_{1}\to s_{1}'}$${\displaystyle (s_{1}',s_{2})\not \in R}$${\displaystyle s_{2}u_{1}\cdots u_{n}s_{2}'}$${\displaystyle n\geq 0}$${\displaystyle (s_{1},u_{i})}$${\displaystyle (s_{1}',s_{2}')}$
3. が有効な遷移であり、がそうでない場合、各ペアがRにあり、がRにあるような有限パスフラグメント（ ）が存在する。${\displaystyle s_{2}\to s_{2}'}$${\displaystyle (s_{1},s_{2}')\not \in R}$${\displaystyle s_{1}v_{1}\cdots v_{n}s_{1}'}$${\displaystyle n\geq 0}$${\displaystyle (v_{i},s_{2})}$${\displaystyle (s_{1}',s_{2}')}$

一般化である発散スタッターバイシミュレーションは、線形時相論理演算子「next」を使用するステートメントが真理値を変更する可能性があるというトレードオフを伴い、システムの状態空間を単純化するために使用できます。 ^[2]堅牢なスタッターバイシミュレーションは、システム内の遷移に関する不確実性を許容します。^[3]