An Expressive Extension of TLC

A temporal logic of causality (TLC) was introduced by Alur, Penczekand Peled in [1]. It is basically a linear time temporal logicinterpreted over Mazurkiewicz traces which allows quantification overcausal chains. Through this device one can directly formulate causalityproperties of distributed systems. In this paper we consider anextension 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 ofthis game prove that the chosen property is not definable in TLC. Wethen show that the same property is definable in TLC. We prove infact the stronger result that TLC is expressively stronger than TLCexactly when the dependence relation associated with the underlyingtrace alphabet is not transitive