LTL is expressively complete for Mazurkiewicz traces

15Citations
Citations of this article
17Readers
Mendeley users who have this article in their library.
Get full text

Abstract

A long standing open problem in the theory of (Mazurkiewicz) traces has been the question whether LTL (Linear Time Logic) is expressively complete with respect to the first order theory. We solve this problem positively for finite and infinite traces and for the simplest temporal logic, which is based only on next and until modalities. Similar results were established previously, but they were all weaker, since they used additional past or future modalities. Another feature of our work is that our proof is direct and does not use any reduction to the word case.

Cite

CITATION STYLE

APA

Diekert, V., & Gastin, P. (2000). LTL is expressively complete for Mazurkiewicz traces. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1853, pp. 211–223). Springer Verlag. https://doi.org/10.1007/3-540-45022-x_18

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free