Pure future local temporal logics are expressively complete for Mazurkiewicz traces (Q859824)

The paper establishes expressive completeness of the pure future local temporal logic on Mazurkiewicz traces with respect to first-order definable trace languages. These are known to be aperiodic, so the main result follows from the proof that every aperiodic trace language is definable in pure future local temporal logic based on \textit{exists-next} and \textit{until} only. The proof and the result generalize \textit{T. Wilke}'s corresponding result on finite words [``Classifying discrete temporal properties'', Lect. Notes Comput. Sci. 1563, 32--46 (1999; Zbl 0926.03018)].