An elementary expressively complete temporal logic for Mazurkiewicz traces

In contrast to the classical setting of sequences, no temporal logic has yet been identified over Mazurkiewicz traces that is equivalent to first-order logic over traces and yet admits an elementary decision procedure. In this paper, we describe a local temporal logic over traces that is expressively complete and whose satisfiability problem is in Pspace. Contrary to the situation for sequences, past modalities are essential for such a logic. A somewhat unexpected corollary is that first-order logic with three variables is expressively complete for traces