Madhavan Mukund

An Elementary Expressively Complete Temporal Logic for Mazurkiewicz Traces

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

  • Download PDF.