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. © 2002 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Gastin, P., & Mukund, M. (2002). An elementary expressively complete temporal logic for Mazurkiewicz traces. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2380 LNCS, pp. 938–949). Springer Verlag. https://doi.org/10.1007/3-540-45465-9_80
Mendeley helps you to discover research relevant for your work.