Let be a labelled state transition system (LTS). Recall that for each label , there is an associated binary relation on . Single out a label , and call it the silent step. Define the following relations:
Finally, for any label , let
Definition. Let and be two labelled state transition systems, with the silent step. A relation is called a weak simulation if whenever and any labelled transition , there is a state such that and . is a weak bisimulation if both and its converse are weak simulations.
|Date of creation||2013-03-22 19:30:55|
|Last modified on||2013-03-22 19:30:55|
|Last modified by||CWoo (3771)|