A Temporal Logic for Event Structures

The formalism of temporal logic has been suggested as an appropriate tool for specifying and proving properties of distributed programs It has become clear that the modalities of temporal logic are well suited for capturing the dynamic properties of distributed programs and systems. Originally, temporal logic was designed in order to analyse and reason about time sequences in general (for example, by Emerson and Halpern. 1985, 1986; Lamport, 1980; Gabbay et al., 1980; Pnueli, 1981). In most of the papers in the area of temporal logic concurrency is represented in terms of an arbitrary nondeterministic interleaving. Because of that the difference between concurrency and non-determinism is lost. This is quite acceptable for many pur-poses, but not always, as shown by Mazurkiewicz et al. (1988). A maior consequence, however, is that one is forced to attach formulas to the global states of a distributed system (program). In general, it is very difficult, if not impossible, to observe such global states; parts of the global state may be changing simultaneously due to independent actions carried out on two separate locations. So, we need a formalism which deals only with local states. In this formalism we incorporate operators representing the relations of causality and conflict.