A temporal logic for causality (TLC) is introduced. The logic is interpreted over causal structures corresponding to partial order executions of programs. For causal structures describing the behavior of a finite fixed set of processes, a TLC-formula can, equivalently, be interpreted over their linearizations. The main result of the paper is a tableau construction that gives a singly-exponential translation from a TLC formula $\varphi$ to a Streett automaton that accepts the set of linearizations satisfying $\varphi$. This allows both checking the validity of TLC formulas and model-checking of program properties. As the logic TLC does not distinguish among different linearizations of the same partial order execution, {\em partial order reduction\/} techniques can be applied to alleviate the state-space explosion problem of model-checking.
Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995), pp. 90--100.