The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
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 omega . In particular, automata operating on words of length omega *n, n in omega 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 omega *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.>
@misc{godefroid1991partial,
title = {A partial approach to model checking},
author = {Patrice Godefroid and Pierre Wolper},
year = {1991},
journal = {Proceedings - Symposium on Logic in Computer Science},
publisher = {Institute of Electrical and Electronics Engineers},
pages = {406--415},
doi = {10.1109/lics.1991.151664},
}
This record lives at https://refs.drheap.org/godefroid1991partial/ and will keep
doing so. It used to be called godefroid2002partial, and those addresses still resolve to this one.