I&C Journal 1994 Journal Article
A Partial Approach to Model Checking
- P. Godefroid
- P. Wolper
This paper presents a model-checking method for linear-time temporal logic that can avoid most of the state explosion due to the modeling of concurrency by interleaving. The method relies on the concept of Mazurkiewicz′s trace as a semantic basis and uses automata-theoretic techniques, including automata that operate on words of ordinality higher than ω.