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

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

Table of contents |

2 Similarity of separate transition systems 3 See also |

Given a labelled state transition system (S, &Lambda, &rarr), a *simulation* relation is a binary relation R over S (i.e. R &sube S × S) such that for every pair of elements p, q &isin S, if (p,q)&isin R then for all &alpha &isin &Lambda, and for all p' &isin S,

implies that there is a q' &isin S such that

and (p',q') &isin R.

Given two states p and q in S, p *simulates* q, written q &le p if there is a simulation R such that (q, p) &isin R. In such case p and q are said to be *similar* and &le is called the *similarity* relation.

The similarity relation &le is a preorder. Furthermore, it is the largest simulation relation over a given transition system.

When comparing two different transition systems (S', &Lambda', &rarr') and (S' ', &Lambda' ', &rarr' '), the basic notions of simulation and similarity can be used by forming the disjoint composition of the two machines, (S, &Lambda, &rarr) with S = S' &cup S' ', &Lambda = &Lambda' &cup &Lambda' ' and &rarr = &rarr' &cup &rarr' ', where &cup is the disjoint union operator between sets.

- State transition systems
- Bisimulation
- Coinductive definitions
- Operational semantics