Equivalence preserving transformations for timed transition models

A modified version of Ostroff's (1989, 1990) timed transition models (TTMs), along with the author's adaptation of Milner's (1980, 1989) observation equivalence to TTMs, is introduced. An informal set of 'behavior preserving' transformations is developed. It is shown to be consistent for proving observation equivalence, and is applied to solve an industrial real-time software verification problem. The incompleteness of a given set of transformations is briefly discussed.<>