Simulation (computer science)

Given a labelled state transition system (${\displaystyle S}$, ${\displaystyle \Lambda }$, →), where ${\displaystyle S}$ is a set of states, ${\displaystyle \Lambda }$ is a set of labels and → is a set of labelled transitions (i.e., a subset of ${\displaystyle S\times \Lambda \times S}$), a relation ${\displaystyle R\subseteq S\times S}$ is a simulation if and only if for every pair of states ${\displaystyle (p,q)}$ in ${\displaystyle R}$ and all labels α in ${\displaystyle \Lambda }$:

if ${\displaystyle p{\overset {\alpha }{\rightarrow }}p'}$, then there is ${\displaystyle q{\overset {\alpha }{\rightarrow }}q'}$ such that ${\displaystyle (p',q')\in R}$

Equivalently, in terms of relational composition:

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

Given two states ${\displaystyle p}$ and ${\displaystyle q}$ in ${\displaystyle S}$, ${\displaystyle p}$ can be simulated by ${\displaystyle q}$, written ${\displaystyle p\,\leq \,q}$, if and only if there is a simulation ${\displaystyle R}$ such that ${\displaystyle (p,q)\in R}$. The relation ${\displaystyle \leq }$ is called the simulation preorder, and it is the union of all simulations: ${\displaystyle (p,q)\in \,\leq \,}$ precisely when ${\displaystyle (p,q)\in R}$ for some simulation ${\displaystyle R}$.

The set of simulations is closed under union;[Note 1] therefore, the simulation preorder is itself a simulation. Since it is the union of all simulations, it is the unique largest simulation. Simulations are also closed under reflexive and transitive closure; therefore, the largest simulation must be reflexive and transitive. From this follows that the largest simulation — the simulation preorder — is indeed a preorder relation.[1] Note that there can be more than one relation which is both a simulation and a preorder;[Note 2] the term simulation preorder refers to the largest one of them (which is a superset of all the others).

Two states ${\displaystyle p}$ and ${\displaystyle q}$ are said to be similar, written ${\displaystyle p\leq \geq q}$, if and only if ${\displaystyle p}$ can be simulated by ${\displaystyle q}$ and ${\displaystyle q}$ can be simulated by ${\displaystyle p}$. Similarity is thus the maximal symmetric subset of the simulation preorder, which means it is reflexive, symmetric, and transitive; hence an equivalence relation. However, it is not necessarily a simulation, and precisely in those cases when it is not a simulation, it is strictly coarser than bisimilarity (meaning it is a superset of bisimilarity).[Note 3] To witness, consider a similarity which is a simulation. Since it is symmetric, it is a bisimulation. It must then be a subset of bisimilarity, which is the union of all bisimulations. Yet it is easy to see that similarity is always a superset of bisimilarity. From this follows that if similarity is a simulation, it equals bisimilarity. And if it equals bisimilarity, it is naturally a simulation (since bisimilarity is a simulation). Therefore, similarity is a simulation if and only if it equals bisimilarity. If it does not, it must be its strict superset; hence a strictly coarser equivalence relation.

When comparing two different transition systems (S', Λ', →') and (S", Λ", →"), the basic notions of simulation and similarity can be used by forming the disjoint composition of the two machines, (S, Λ, →) with S = S' ∐ S", Λ = Λ' ∪ Λ" and → = →' ∪ →", where ∐ is the disjoint union operator between sets.

• State transition system
• Bisimulation
• Coinduction
• Operational semantics

1. Park, David (1981). "Concurrency and Automata on Infinite Sequences" (PDF). In Deussen, Peter (ed.). Proceedings of the 5th GI-Conference, Karlsruhe. Lecture Notes in Computer Science. Vol. 104. Springer-Verlag. pp. 167–183. doi:10.1007/BFb0017309. ISBN 978-3-540-10576-3.
2. van Glabbeek, R. J. (2001). "The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes". Handbook of Process Algebra. Elsevier. pp. 3–99.