From local to global temporal logics over Mazurkiewicz traces

We review some results on global and local temporal logic on Mazurkiewicz traces. Our main contribution is to show how to derive the expressive completeness of global temporal logic with respect to first-order logic [V. Diekert, P. Gastin, LTL is expressively complete for Mazurkiewicz traces, J. Comput. System Sci. 64 (2002) 396–418] from the similar result on local temporal logic [V. Diekert, P. Gastin, Pure future local temporal logics are expressively complete for Mazurkiewicz traces, in: M. Farach-Colton (Ed.), Proc. LATIN’04, Lecture Notes in Computer Science, Vol. 2976, Springer, Berlin, 2004, pp. 232–241, Full version available as Research Report LSV-05-22, Laboratoire Spécification et Vérification, ENS Cachan, France].