Simulation preorder

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,

${\displaystyle p{\overset {\alpha }{\rightarrow }}p'}$

implies that there is a q' ∈ S such that

${\displaystyle q{\overset {\alpha }{\rightarrow }}q'}$

and (p', q') ∈ R.

Equivalently, in terms of relational composition:

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

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.

Two states p and q are said to be similar, written p ≤≥ q, if p simulates q and q simulates p. Similarity is an equivalence relation, but it is coarser than bisimilarity.

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 systems
• 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. 104. Springer-Verlag. pp. 167–183. doi:10.1007/BFb0017309. ISBN 978-3-540-10576-3.
2. Milner, Robin (1989). Communication and Concurrency. Prentice Hall. ISBN 0-13-114984-9.
3. 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.