A Partial Approach to Model Checking

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 ω.

Authors

• P. Godefroid
• P. Wolper

Keywords

No keywords are indexed for this paper.