An Expressive Extension of TLC

Jesper G. Henriksen

Abstract


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.

Full Text:

PDF


DOI: http://dx.doi.org/10.7146/brics.v6i26.20095
This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.
OK


ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library