When dealing with concurrent systems, one possible approach is to reduce them to sequential systems, by considering all linearizations. Then, one can apply techniques and tools developed for sequential systems. Using this approach, however, one is faced with a combinatorial problem.

In order to avoid a combinatorial explosion, one could try to work directly on concurrent systems. Using this approach, one could take advantage of the large amount of research recently devoted to the study of temporal logics for concurrency. A main goal of this research is to find a temporal logic that is expressive enough to ensure that all desired specifications can be formalized.

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, generalizing the results of W. Ebinger [2], Thiagarajan and Walukiewicz [3], and Wilke [4], it is proved that linear temporal logic for finite and infinite traces is expressively complete, with respect to the first order theory.