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.
展开▼
机译：最近，Thiagarajan和Walukiewicz为Mazurkiewicz迹线定义了一种新的时间逻辑，表示为LTrL [15]。他们表明，这种逻辑在表达能力上与有限迹线和无限迹线的一阶理论相同，因此填补了该理论中的一个突出空白。我们在本文中提出了仅在有限迹线情况下此结果的全新的代数证明。我们的证明概括了conhen，perrin和Pin在有限序列上的工作[2]，并使用了花圈上的花圈乘积原理的新扩展作为基本工具[7]。作为我们证明的主要结果，我们表明，仅处理有限迹线时，不需要过去的模态即可获得表达上完整的逻辑。确切地说，我们证明通过不使用过去的模块化从LTrL获得的逻辑LTrL sub red具有与有限迹上的一阶理论相同的表示能力。
展开▼
