Given two labelled state transition systems (LTS) , , a binary relation is called a simulation if whenever and , then there is a such that and . An LSTS is similar to an LTS if there is a simulation .
if is similar to and is similar to , then is similar to :
Let , , and be LSTS, and suppose with , where and are simulations. Then there is an such that and . Since is a simulation, there is an such that . But then since is a simulation, there is a such that . As a result, is a simulation. ∎
a union of simulations is a simulation.
Let be the union of simulations , where , and suppose , with . Then for some . Since is a simulation, there is a state such that and . So and therefore is a simulation. ∎
A binary relation between and is a bisimulation if both and its converse are simulations. A bisimulation is also called a strong bisimulation, in contrast with weak bisimulation. When there is a bisimulation between the state sets of two LTS, we say that the two systems are bisimilar, or strongly bisimilar. By abuse of notation, we write to denote that is bisimilar to .
Then the binary relation can be extended to a binary relation from to , still denoted by , as
for any and . In other words, iff for any , there is a such that and for any , there is an such that . Now, for any and , let
We can similar define function . So a binary relation between and is a bisimilation iff for any such that , we have for any .
Let , , and be LTS. The following are some basic properties of bisimulation:
The identity relation is a bisimilation on any LTS, since is a simulation and is just .
If is bisimilar to via , then is bisimilar to via , since both and are simulations.
If and , then , since and are both simulations according to the argument above.
A union of bisimilations is a bisimilation.
Let be the union of bisimulations , where . Then is a simulation by the argument above. Now, suppose and , then . Then for some . So . Since is a bisimulation, so is , and therefore for some state , and . This means that , implying that is a simulation. Hence is a bisimulation. ∎
The union of all bisimilations on an LTS is a bisimulation that is also an equivalence relation.
For an LTS , let be the union of all bisimulations on . Then is a bisimulation by the previous result. Since is a bisimulation on , is reflexive. If , for some bisimulation on . Then is a bisimulation and therefore implies that , so that is symmetric. Finally, if and , then and for some bisimulations and . So is a bisimulation. Since , and therefore is transitive. ∎
For an LTS , let be the maximal bisimulation on as defined above. Since is an equivalence relation, we can form an equivalence class for each state . Let be the set of all such equivalence classes: . Define on by
|Date of creation||2013-03-22 19:23:14|
|Last modified on||2013-03-22 19:23:14|
|Last modified by||CWoo (3771)|