Paper: An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces (at LICS 1997)

Authors: P. S. Thiagarajan Igor Walukiewicz

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.

BibTeX

  @InProceedings{ThiagarajanWalukiew-AnExpressivelyCompl,
    author = 	 {P. S. Thiagarajan and Igor Walukiewicz},
    title = 	 {An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces},
    booktitle =  {Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS 1997)},
    year =	 {1997},
    month =	 {June}, 
    pages =      {183--194},
    location =   {Warsaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }