An Expressive Extension of TLC

Forfattere

  • Jesper G. Henriksen

DOI:

https://doi.org/10.7146/brics.v6i26.20095

Resumé

A temporal logic of causality (TLC) was introduced by Alur, Penczek
and Peled in [1]. It is basically a linear time temporal logic
interpreted over Mazurkiewicz traces which allows quantification over
causal chains. Through this device one can directly formulate causality
properties of distributed systems. In this paper we consider an
extension of TLC by strengthening the chain quantification operators.
We show that our logic TLC  adds to the expressive power of TLC.
We do so by defining an Ehrenfeucht-Fraissé game to capture the expressive
power of TLC. We then exhibit a property and by means of
this game prove that the chosen property is not definable in TLC. We
then show that the same property is definable in TLC. We prove in
fact the stronger result that TLC is expressively stronger than TLC
exactly when the dependence relation associated with the underlying
trace alphabet is not transitive.

Downloads

Publiceret

1999-01-26

Citation/Eksport

Henriksen, J. G. (1999). An Expressive Extension of TLC. BRICS Report Series, 6(26). https://doi.org/10.7146/brics.v6i26.20095

Nummer

Nr. 26 (1999): RS-26 An Expressive Extension of TLC

Sektion

Artikler

Licens

Authors who publish with this journal agree to the following terms:

    1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.

    1. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.

  1. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).