Summary: 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 \(\omega\).