Abstract
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 expressive power to the first order theory of finite and infinite traces thus filling a prominent gap in the theory.
We propose in this paper a entirely new, algebraic, proof of this result in the case of finite traces only. Our proof generalizes Cohen, Perrin and Pin's work on finite sequences [2], using as a basic tool 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 the logic LTrL red, obtained from LTrL by not using the past modularity, has the same expressive power as the first order theory on finite traces.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, D. Peled, and W. Penczek. Model-checking of causality properties. In Proceedings of LICS'95, pages 90–100, 1995.
J. Cohen, D. Perrin, and J. E. Pin. On the expressive power of temporal logic. Journal of Computer and System Sciences, 46:271–295, 1993.
V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.
W. Ebinger. Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. Dissertation, Institut für Informatik, Universität Stuttgart, 1994.
S. Eilenberg. Automata, Languages, and Machines, volume B. Academic Press, New York and London, 1976.
P. Godefroid. Partial-order methods for the verification of concurrent systems. In LNCS 1032, pages 176–185. Springer, 1996.
G. Guaiana, R. Meyer, A. Petit, and P. Weil. An extension of the wreath product principle to traces. to appear, 1997.
G. Guaiana, A. Restivo, and S. Salemi. On aperiodic trace languages. In Proceedings of STACS'91, number 480 in Lecture Notes in Computer Science, pages 76–88, 1991.
A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.
D. Peled. Partial-order reductions: model checking using representatives. In Proceedings of MFCS'96, number 1113 in Lecture Notes in Computer Science, pages 93–112, 1996.
A. Pnueli. The temporal logics of programs. In Proceedings of the l8th IEEE FOCS, 1977, pages 46–57, 1977.
R. Ramanujam. Locally linear time temporal logic. In Proceedings of LICS'96, pages 118–128, 1996.
H. Straubing. The wreath product and its applications. In Proceedings of the LITP Spring School on Theoretical Computer Science (in LNCS vol. 386), pages 15–24, 1988.
P. S. Thiagarajan. A trace based extension of linear time temporal logic. In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS'94), pages 438–447, 1994.
P. S. Thiagarajan and I. Walukiewicz. An expressively complete linear time temporal logic for mazurkiewicz traces. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97), 1997.
W. Thomas. Automata on infinite objects. In J. v. Leeuwen, editor, Handbook of Theoretical Computer Science, pages 133–191. Elsevier Science Publishers, 1990.
A. Valmari. A stubborn attack on state explosion. In Formal Methods in System Design, pages 1:297–322, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag
About this paper
Cite this paper
Meyer, R., Petit, A. (1998). Expressive completeness of LTrL on finite traces: An algebraic proof. In: Morvan, M., Meinel, C., Krob, D. (eds) STACS 98. STACS 1998. Lecture Notes in Computer Science, vol 1373. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028588
Download citation
DOI: https://doi.org/10.1007/BFb0028588
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64230-5
Online ISBN: 978-3-540-69705-3
eBook Packages: Springer Book Archive