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.
Given a labelled state transition system (S, Λ, →), a simulation relation is a binary relation R over S (i.e. R ⊆ S × S) such that for every pair of elements (p,q) ∈ R, for all α ∈ Λ, and for all p' ∈ S,
implies that there is a q' ∈ S such that
and (p',q') ∈ R.
Equivalently, in terms of relational composition:
Given two states p and q in S, q simulates p, written p ≤ q if there is a simulation R such that (p, q) ∈ R. The relation ≤ is a preorder, and is usually called the simulation preorder. It is the largest simulation relation over a given transition system.
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.
- Park, David (1981). "Concurrency and Automata on Infinite Sequences". In Deussen, Peter. Proceedings of the 5th GI-Conference, Karlsruhe. Lecture Notes in Computer Science. 104. Springer-Verlag. pp. 167–183. doi:10.1007/BFb0017309. ISBN 978-3-540-10576-3.
- Milner, Robin (1989). Communication and Concurrency. Prentice Hall. ISBN 0-13-114984-9.
- 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.