Model-checking of causality properties

A temporal logic for causality (T_LC) 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 T_LC-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 T_LC formula ψ to a Streett automaton that accepts the set of linearizations satisfying ψ. This allows both checking the validity of T_LC formulas and model-checking of program properties. As the logic T_LC does not distinguish among different linearizations of the same partial order execution, partial order reduction techniques can be applied to alleviate the state-space explosion problem of model-checking