シミュレーション（コンピュータサイエンス）

理論計算機科学において、シミュレーションとは、あるシステムが他のシステムをシミュレートするという意味で同じように動作するシステムを関連付ける状態遷移システム間の関係です。

直感的に言えば、システムは、他のシステムの動きをすべて一致させることができれば、他のシステムをシミュレートします。

基本的な定義は、1 つの遷移システム内の状態を関連付けますが、対応するコンポーネントの 分離した結合で構成されるシステムを構築することで、2 つの個別の遷移システムを関連付けるように簡単に適応できます。

ラベル付き状態遷移システム( , , →)が与えられた場合( は状態の集合、はラベルの集合、 → はラベル付き遷移の集合 (つまり のサブセット))、関係がシミュレーションであるための必要条件は、内のすべての状態のペアと 内のすべてのラベル λに対して次の条件を満たす場合のみです。 ${\displaystyle S}$${\displaystyle \Lambda}$${\displaystyle S}$${\displaystyle \Lambda}$${\displaystyle S\times \Lambda \times S}$${\displaystyle R\subseteq S\times S}$${\displaystyle (p,q)}$${\displaystyle R}$${\displaystyle \Lambda}$

ならば、​${\displaystyle p{\overset {\lambda }{\rightarrow }}p'}$${\displaystyle q{\overset {\lambda }{\rightarrow }}q'}$${\displaystyle (p',q')\in R}$

同様に、関係構成の観点からは、

${\displaystyle R^{-1}\,;\,{\overset {\lambda }{\rightarrow }}\quad {\subseteq }\quad {\overset {\lambda }{\rightarrow }}\,;\ ,R^{-1}}$

における2 つの状態と が与えられた場合、となるシミュレーションが存在する場合に限り、 （ と表記）によってシミュレートできます。この関係はシミュレーションの順序付けと呼ばれ、すべてのシミュレーションの和集合です。つまり、あるシミュレーション に対して のとき、まさに となります。 ${\displaystyle p}$${\displaystyle q}$${\displaystyle S}$${\displaystyle p}$${\displaystyle q}$${\displaystyle p\,\leq \,q}$${\displaystyle R}$${\displaystyle (p,q)\in R}$${\displaystyle \leq}$${\displaystyle (p,q)\in \,\leq \,}$${\displaystyle (p,q)\in R}$${\displaystyle R}$

シミュレーションの集合は和集合で閉じている。^{[注 1]}したがって、シミュレーションの事前順序はそれ自体がシミュレーションである。これはすべてのシミュレーションの和集合であるため、唯一の最大のシミュレーションである。シミュレーションは反射的かつ推移的な閉包でも閉じているため、最大のシミュレーションは反射的かつ推移的である必要がある。このことから、最大のシミュレーション、つまりシミュレーションの事前順序は確かに事前順序関係であることがわかる。^[1]シミュレーションであり事前順序でもある関係が複数存在する可能性があることに注意してください。^{[注 2]}シミュレーションの事前順序という用語は、それらのうち最大のもの（他のすべてのスーパーセット）を指します。

2 つの状態と は、が でシミュレートでき、 がでシミュレートできる場合に限り、類似 （ と表記）であるとされます。したがって、類似性はシミュレーション前順序の最大の対称部分集合であり、反射的、対称的、推移的であることを意味します。したがって、同値関係 です。ただし、必ずしもシミュレーションではなく、シミュレーションでない場合は、厳密には双類似性よりも粗いです（つまり、双類似性のスーパーセットです）。^{[注 3]} 証拠として、シミュレーションである類似性を考えてみましょう。対称であるため、双シミュレーションです。したがって、それは双類似性のサブセットでなければならず、双類似性はすべての双シミュレーションの和集合です。しかし、類似性は常に双類似性のスーパーセットであることは容易にわかります。このことから、類似性がシミュレーションである場合、それは双類似性と等しいことがわかります。そして、それが双類似度に等しい場合、それは当然シミュレーションです (双類似度はシミュレーションであるため)。したがって、類似度がシミュレーションとなるのは、それが双類似度に等しい場合のみです。そうでない場合は、その厳密なスーパーセットである必要があります。したがって、厳密に粗い同値関係になります。 ${\displaystyle p}$${\displaystyle q}$${\displaystyle p\leq \geq q}$${\displaystyle p}$${\displaystyle q}$${\displaystyle q}$${\displaystyle p}$

2 つの異なる遷移システム (S', Λ', →') と (S", Λ", →") を比較する場合、シミュレーションと類似性の基本概念は、2 つのマシンの互いに素な合成 (S, Λ, →) を形成することによって使用できます。この場合、S = S' ∐ S", Λ = Λ' ∪ Λ"、→ = →' ∪ →", となります。ここで、∐ はセット間の 互いに素な和集合演算子です。

• 状態遷移システム
• バイシミュレーション
• 共誘導
• 操作的意味論

1. Park, David (1981)。「無限シーケンス上の並行性とオートマトン」(PDF)。Deussen, Peter (編)。第 5 回 GI カンファレンスの議事録、カールスルーエ。コンピュータ サイエンスの講義ノート。第 104 巻。Springer -Verlag。pp . 167–183。doi :10.1007/ BFb0017309。ISBN 978-3-540-10576-3。
2. van Glabbeek, RJ (2001)。「線形時間 - 分岐時間スペクトル I: 具体的で連続的なプロセスの意味論」。プロセス代数ハンドブック。エルゼビア。pp. 3–99。