Editing Simulation (computer science)

In [[theoretical computer science]] a '''simulation''' is a [[Relation (mathematics)|relation]] between [[state transition system]]s associating systems that behave in the same way in the sense that one system ''simulates'' the other.

Intuitively, a system simulates another system if it can match all of its moves.

The basic definition relates states within one transition system, but this is easily adapted to relate two separate transition systems by building a system consisting of the [[disjoint union]] of the corresponding components.

==Formal definition==
Given a [[state transition system|labelled state transition system]] (<math>S</math>, <math>\Lambda</math>, &rarr;),
where <math>S</math> is a set of states, <math>\Lambda</math> is a set of labels and &rarr; is a set of labelled transitions (i.e., a subset of <math>S \times \Lambda \times S</math>),
a relation <math>R \subseteq S \times S</math> is a '''simulation''' if and only if for every pair of states <math>(p,q)</math> in <math>R</math> and all labels &lambda; in <math>\Lambda</math>:

: '''if <math>p \overset{\lambda}{\rightarrow} p'</math>, then there is <math>q \overset{\lambda}{\rightarrow} q'</math> such that <math>(p',q') \in R</math>'''

Equivalently, in terms of [[Composition of relations|relational composition]]:
:<math>R^{-1}\,;\, \overset{\lambda}{\rightarrow}\quad {\subseteq}\quad \overset{\lambda}{\rightarrow}\,;\, R^{-1}</math>

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

The set of simulations is closed under union;<ref group="Note">
    Meaning the union of two simulations is a simulation.
</ref> 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 closure|reflexive]] and [[transitive closure|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|preorder relation]].<ref>{{cite book |last=Milner |first=Robin |authorlink = Robin Milner|title=Communication and Concurrency |year=1989 |isbn=0131149849 |publisher=Prentice-Hall, Inc. |location=USA}}</ref> Note that there can be more than one relation that is both a simulation and a preorder;<ref group=Note>Consider the relations <math>\{\}</math> and <math>\{(0, 0)\}</math>—each is both a simulation and a preorder.</ref> the term ''simulation preorder'' refers to the largest one of them (which is a superset of all the others).

Two states <math>p</math> and <math>q</math> are said to be '''similar''', written <math>p \leq\geq q</math>, if and only if <math>p</math> can be simulated by <math>q</math> and <math>q</math> can be simulated by <math>p</math>. 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).<ref group="Note">For an example, see '''Fig. 1''' in {{cite journal
|last1 = Champarnaud
|first1 = J.-M
|last2 = Coulon
|first2 = F.
|title = NFA reduction algorithms by means of regular inequalities
|journal = [[Theoretical Computer Science (journal)|Theoretical Computer Science]]
|volume = 327
|number = 3
|pages = 241–253
|year = 2004
|issn = 0304-3975
|doi = 10.1016/j.tcs.2004.02.048
|doi-access = free
}}</ref>
To witness, consider a similarity that ''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.

==Similarity of separate transition systems==
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.

==See also==
* [[State transition system]]
* [[Bisimulation]]
* [[Coinduction]]
* [[Operational semantics]]

== Notes==
{{reflist|group=Note}}

== References ==
# {{Cite conference
 | first = David
 | last = Park
 | year = 1981
 | title = Concurrency and Automata on Infinite Sequences
 | book-title = Proceedings of the 5th GI-Conference, Karlsruhe
 | series = [[Lecture Notes in Computer Science]]
 | editor = Deussen, Peter
 | pages = 167–183
 | volume = 104
 | publisher = [[Springer-Verlag]]
 | isbn = 978-3-540-10576-3
 | doi = 10.1007/BFb0017309
| url = http://wrap.warwick.ac.uk/47224/1/WRAP_Park_cs-rr-035.pdf
 }}
# {{Cite conference
 | last = van Glabbeek
 | first = R. J.
 | title = The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes
 | book-title = Handbook of Process Algebra
 | chapter-url = http://boole.stanford.edu/pub/spectrum1.pdf.gz
 | chapter = 1
 | pages = 3–99
 | year = 2001
 | publisher = Elsevier
}}

{{DEFAULTSORT:Simulation Preorder}}
[[Category:Theoretical computer science]]
[[Category:Transition systems]]