Logic in Computer Science, Symposium on (1997)

Warsaw, POLAND

June 29, 1997 to July 2, 1997

ISSN: 1043-6871

ISBN: 0-8186-7925-5

pp: 183

P.S. Thiagarajan , SPIC Mathematical Institute

I. Walukiewicz , Institute of Informatics, Warsaw University

ABSTRACT

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.

INDEX TERMS

CITATION

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.

doi:10.1109/LICS.1997.614946

CITATIONS