Simulation Preorder and Bisimilarity
22 Aug 2012
Simulation Preorder is a Relation Defined in the context of Labled Transition System!
- Labled Transition system is consist of states and transition between these states which are labled!
- Relation is actually a collection(set) of ordered pairs!
So Simulation Preorder is a set of ordered pairs! (Which ones?) Those which are similar in the sense that they are acting like eachother regarding to their transitions. In another word take state A and B if any outgoing transition(edge) from these states goes to the same state, (A, B) is in the Simulation Preorder Relation or A and B has Simulation Preorder Relation.
in above sentence by same state we mean that they are in simulation Preorder Relation. with this consideration we see that Simulation Preorder relation definition is somehow recursive. But since this relation is Reflexive so for constructing it we might be able to start with reflexive pairs in the Relation to built it up.
Wikipedia:
- 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.
- Two states p and q are said to be similar if p simulates q and q simulates p. Similarity is an equivalence relation, but it is coarser than bisimilarity.
- Bisimilarity: Given a labelled state transition system (S,∧,→) , a bisimulation relation is a binary relation R over S (i.e.,R ⊆ S ×S ) such that both R-1 and R are Simulation Preorder.