Paper: Model-Checking of causality properties (at LICS 1995)

Authors: Rajeev Alur Doron A. Peled Wojciech Penczek

Abstract

A temporal logic for causality (TLC) is introduced. The logic is interpreted over causal structures corre- sponding 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 cp to a Streett automaton that accepts the set of linearizations satisfying cp. 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, partial order reduction techniques can be applied to alleviate the state-space explosion problem of model-checking.

BibTeX

  @InProceedings{AlurPeledPenczek-ModelCheckingofcaus,
    author = 	 {Rajeev Alur and Doron A. Peled and Wojciech Penczek},
    title = 	 {Model-Checking of causality properties},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {90--100},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }