Open AccessAn Expressive Extension of TLC
Author(s) -
Jesper G. Henriksen
Publication year - 1999
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v6i26.20095
Subject(s) - expressive power , extension (predicate logic) , property (philosophy) , alphabet , causality (physics) , mathematics , power (physics) , discrete mathematics , computer science , theoretical computer science , programming language , philosophy , physics , linguistics , epistemology , quantum mechanics
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.