Logic in Computer Science (LICS 1996)

Paper: Partial-Order Methods for Model Checking: From Linear Time to Branching Time (at LICS 1996)

Authors: Bernard Willems Pierre Wolper

Abstract

Partial-order methods make it possible to check properties of a concurrent system by state-space exploration without considering all interleavings of independent concurrent events. They have been applied to linear-time model checking, but so far only limited results are known about their applicability to branching-time model checking. In this paper, we introduce a general technique for lifting partial-order methods from linear-time to branching-time logics. This technique is shown to be applicable both to reductions that are applied to the structure representing the program before running the model checking procedure, as well as to reductions that can be obtained when model checking is done in an automata-theoretic framework. The latter are extended to branching-time logics by using the model-checking framework based on alternating automata introduced by Bernholtz, Vardi and Wolper.

BibTeX

  @InProceedings{WillemsWolper-PartialOrderMethods,
    author = 	 {Bernard Willems and Pierre Wolper},
    title = 	 {Partial-Order Methods for Model Checking: From Linear Time to Branching Time},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {294-303},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }