Logic in Computer Science, Symposium on (1997)
June 29, 1997 to July 2, 1997
P.S. Thiagarajan , SPIC Mathematical Institute
I. Walukiewicz , Institute of Informatics, Warsaw University
A basic result concerning LTL, the propositional temporal logic of linear time, is that it is expressively complete; it is equal in expressive power to the first order theory of sequences. We present here a smooth extension of this result to the class of partial orders known as Mazurkiewicz traces. These partial orders arise in a variety of contexts in concurrency theory and they provide the conceptual basis for many of the partial order reduction methods that have been developed in connection with LTL -specifications.We show that LTrL, our linear time temporal logic, is equal in expressive power to the first order theory of traces when interpreted over (finite and) infinite traces. This result fills a prominent gap in the existing logical theory of infinite traces. LTrL also provides a syntactic characterisation of the so called trace consistent (robust) LTL -specifications. These are specifications expressed as LTL formulas that do not distinguish between different linearisations of the same trace and hence are amenable to partial order reduction methods.
I. Walukiewicz and P. Thiagarajan, "An Exprssively Complete Linear Time Temporal Logic for Mazurkiewicz Traces.," Logic in Computer Science, Symposium on(LICS), Warsaw, POLAND, 1997, pp. 183.