Logic in Computer Science (LICS 1991)

Paper: A partial approach to model checking (at LICS 1991)

Authors: Patrice Godefroid Pierre Wolper

Abstract

A model-checking method for linear-time temporal logic that avoids the state explosion due to the modeling of concurrency by interleaving is presented. The method relies on the concept of the Mazurkiewicz trace as a semantic basis and uses automata-theoretic techniques, including automata that operate on words of ordinality higher than ω. In particular, automata operating on words of length ω×n , n∈ω are defined. These automata are studied, and an efficient algorithm to check whether such automata are nonempty is given. It is shown that when it is viewed as an ω×n automaton, the trace automaton can be substituted for the production automaton in linear-time model checking. The efficiency of the method of P. Godefroid (Proc. Workshop on Computer Aided Verification, 1990) is thus fully available for model checking

BibTeX

  @InProceedings{GodefroidWolper-Apartialapproachtom,
    author = 	 {Patrice Godefroid and Pierre Wolper},
    title = 	 {A partial approach to model checking},
    booktitle =  {Proceedings of the Sixth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1991},
    year =	 1991,
    editor =	 {Giles Kahn},
    month =	 {July}, 
    pages =      {406--415},
    location =   {Amsterdam, The Netherlands}, 
    publisher =	 {IEEE Computer Society Press}
  }