## Model-Checking of Causality Properties

*Rajeev Alur, Doron A. Peled, and
Wojtek Penczek*
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.