A partial approach to model checking

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