Simulazione e doppia simulazione

La nozione di preordine $\sqsubseteq$ introdotta nel capitolo 4 può anche essere intesa come 'meno definito di' nel senso che $p \: \sqsubseteq \: q$ si può leggere come '$p$ è meno definito di $q$', $p$ può compiere meno azioni di $q$ o, simmetricamente, $q$ può fare almeno tante azioni quante ne fa $p$ (tendenzialmente di più); si può anche intendere che p è simulabile da q:

Definizione 5..13 (Simulazione)   $p \: \sqsubseteq \: q$ sse $\forall \alpha \: \in \: Act_{\tau}^*$, se $p \stackrel{\alpha}{\longrightarrow} p'$ allora per qualche $q'$ si a che $q \stackrel{\alpha}{\longrightarrow} q' \: \land \: p' \: \sqsubseteq \: q'$.

$$P = \alpha.\beta.nil \quad Q=\alpha.nil + \alpha.\beta.nil \quad \Rightarrow \quad P \sqsubseteq Q \quad ($$ma anche $$Q \sqsubseteq P)$$

Naturalmente, essendo un preordine, della simulazione se ne può prendere il kernel ed ottenere la doppia simulazione $\simeq$, la quale però non coincide con la bisimulazione $\sim$, vediamo perchè con un esempio: prendendo sempre gli stessi processi definiti sopra, si vede che questi sono doppiamente simili ma non sono bisimili in quanto $P \stackrel{\alpha}{\longrightarrow} nil \: \land \: Q \stackrel{\alpha}{\longrightarrow} Q'$ ma $nil \not\sim Q'$