Préordre de simulation
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.
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, implique qu'il existe q' ∈ S tel que 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é.
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.
Voir aussi
- Système de transition d'états
- Bisimulation
- Définition coinductive
- Sémantique opérationnelle