|
An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz
Traces
P. S. Thiagarajan December 1996 |
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 distiguish between different linearizations of the same trace and hence are amenable to partial order reduction methods
Available as PostScript, PDF, DVI. |