What is the process of trace equivalence verification for given 2 FSMs?

Category: Software testing.

Used in the LTSA (Labelled Transition System Analyser) tool for model based verification of web service composition: http://ift.tt/1G8UArH

Also, what is meant by trace equivalence verification?

To my knowledge, trace is a log of execution of a process. In trace equivalence, do we directly compare the trace obtained for both FSMs?