Refinement checking is an important method in formal verification to convey a refinement relationship between an implementation model and a specification model in the same language.If the specification satisfies certain property and the refinement relationship is strong enough to preserve the property, then implementation satisfies the property.Refinement checking was developed in order to verify different kinds of properties, traces, stables failures and failures/divergence.Refinement checking often relies on the subset construction, thus suffers from state space explosion.Recently, some researchers proposed a simulation based approach for solving the language inclusion problem of NFA, which outperforms the previous methods significantly and can be directly used in traces refinement checking.Base on this advancement, this work further proposes stable failures and failures-divergence refinement checking algorithms based on simulation relations.In addition, this work also extends the idea of trace refinement checking to timed systems, and proposes timed automata traces refinement checking based on simulation relations.Experimental results confirm the efficiency of the presented approaches.