## 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} }