Approximate trace and singleton failures equivalences for transition systems

Established system equivalences for transition systems, such as trace equivalence and failures equivalence, require the observations to be exactly identical. However, an accurate measurement is impossible when interacting with the physical world, hence exact equivalence is restrictive and not robust. Using Baire metric, a generalized framework of transition system approximation is proposed by developing the notions of approximate language equivalence and approximate singleton failures (SF) equivalence. The framework takes the traditional exact equivalence as a special case. The approximate language equivalence is coarser than the approximate SF equivalence, just like the hierarchy of the exact ones. The main conclusion is that the two approximate equivalences satisfy the transitive property, consequently, they can be successively used in transition system approximation.