Open AccessAn Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces
Author(s) -
P. S. Thiagarajan,
Igor Walukiewicz
Publication year - 1996
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v3i62.18563
Subject(s) - trace (psycholinguistics) , concurrency , expressive power , linear temporal logic , temporal logic , partial order reduction , mathematics , reduction (mathematics) , extension (predicate logic) , computer science , class (philosophy) , basis (linear algebra) , variety (cybernetics) , discrete mathematics , theoretical computer science , algorithm , programming language , model checking , artificial intelligence , philosophy , linguistics , geometry
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.