Préordre de simulation

Un article de Wikipédia, l'encyclopédie libre.

En informatique théorique un préordre de simulation est une relation entre systèmes de transition d'états associant des systèmes qui se comportent de la même façon au sens qu'un système simule l'autre.

Intuitivement, un système simule l'autre s'il peut imiter toutes ses actions.

La définition basique relie les états à l'intérieur d'un système de transition, mais c'est facilement adaptable pour mettre en relation deux systèmes de transition séparés en construisant un système consistant en l'union disjointe des composants correspondants.

[modifier] Définition formelle

Étant donné un système de transition d'états étiqueté (S, Λ, →), une relation de simulation est une relation binaire R sur S (c.à.d R ⊆ S × S) telle que pour chaque paire d'éléments p, q ∈ S, si (p,q)∈ R alors pour tout α ∈ Λ, et pour tout p' ∈ S,

$\begin{matrix} & \alpha & \\ p & \rightarrow & p' \\ \end{matrix}$

implique qu'il existe q' ∈ S tel que

$\begin{matrix} & \alpha & \\ q & \rightarrow & q' \\ \end{matrix}$

et (p',q') ∈ R.

Étant donnés deux états p et q dans S, q simule p, noté p ≤ q s'il existe une simulation R telle que (p, q) ∈ R. Dans ce cas, p et q sont dits similaires et ≤ est appelé la relation de similarité.

La relation de similarité ≤ est un pré-ordre. De plus, c'est la plus grande simulation sur un système de transition donné.

[modifier] Similarité de systèmes de transition séparés

Quand on compare deux systèmes de transition différents (S', Λ', →') et (S' ', Λ' ', →' '), les notions basiques de simulation et de similarité peuvent être utilisées en formant la composition disjointe des deux machines, (S, Λ, →) avec S = S' ∪ S' ', Λ = Λ' ∪ Λ' ' et → = →' ∪ →' ', où ∪ est l'opérateur d'union disjointe entre ensembles.