The basic result, due to Kamp, concerning the propositional temporal logic of linear time (LTL) interpreted over sequences is that LTL has the same expressive power as the first order theory of sequences. Unfortunately, using sequences is not a convenient method for considering an application of temporal logic for concurrency problems.

Trace theory [1], initiated by Mazurkiewicz, is one of the most popular settings for studying concurrency. Various temporal logics for traces have recently been extensively studied. In this paper, a restricted LTL (LTrL), with future modalities and past modalities in the restricted form of past constants, is constructed. It is proved that LTrL for finite and infinite traces is expressively complete with respect to the first order theory. The same result for unrestricted LTL is obtained in Diekert and Gastin [2].