Algebraic characterizations of trace and decorated trace equivalences overtree-like structures

Behavioural equivalences of labelled transition systems are characterized i n terms of homomorphic transformations. This permits relying on algebraic t echniques for proving systems properties and reduces equivalence checking o f two systems to studying the relationships among the elements of their str uctures. Different algebraic characterizations of bisimulation-based equiva lences in terms of particular transition system homomorphisms have been pro posed in the literature. Here, it is shown that trace and decorated trace e quivalences can neither be characterized in terms of transition system homo morphisms, nor be defined locally, i.e., only in terms of action sequences of bounded length and of root-preserving maps. However, results similar to those for bisimulation can be obtained for restricted classes of transition systems. For tree-like systems, we present the algebraic characterizations of trace equivalence and of three well-known decorated trace equivalences, namely ready, ready trace equivalence and failure. (C) 2001 Elsevier Scien ce B.V. All rights reserved.