P Gastin and M Mukund
Proc. ICALP '02, Springer LNCS 2382 (2002) 938-949.
© Springer-Verlag Berlin Heidelberg
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.
Keywords Temporal logics, Mazurkiewicz traces, concurrency