Since 2014
An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces
|
|
| Creator |
Thiagarajan, P. S.
Walukiewicz, Igor |
|
| Description |
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.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1996-12-02
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18563
10.7146/brics.v3i62.18563 |
|
| Source |
BRICS Report Series; No 62 (1996): RS-62: An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces
BRICS Report Series; Nr. 62 (1996): RS-62: An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18563/16232
|
|