Very recently a new temporal logic, for Mazurkiewicz traces, denoted LTrL, has been defined by Thiagarajan and Walukiewicz [15]. They have shown that this logic is equal in expresive power to the first order theory of finite and infiinte traces thus filling a prominent gap in the theory. We proposee in this paper a entirely new, algebraic, proof of this esult in the case of finite traces only. Our proof generalizes conhen, perrin and Pin's work on finite sequences[2], using as a basictool a new extension of the wreath product principle on traces[7]. As a major consequence of our proof we show that, when dealing with finite traces only, no past modality is necessary to obtain a expressively complete logic. precisely,we prove that teh logic LTrL sub red, obtained rom LTrL by not using the past modularity, has the same expresive power as the first order theory on finite traces.
展开▼
