Abstract: Formal verification is the growing field of formalizing and verifying specifications for hardware and software systems. One such technique, known as model checking, can exhaustively check a software model for properties written in a specification language, such as Linear Temporal Logic (LTL). For large systems, memory reduction techniques are often used to complete a verification with the available hardware. One reduction technique, that of partial order reduction, has proven useful in aiding verifications, but it limits the expressiveness of LTL specifications.  Due to the phenomenon  of stuttered states in the model's reduced state graph representation, the LTL next operator is not guaranteed to produce correct results when partial order reduction is used. As more casual users begin using model checking, it is important to provide them with a convenient method of writing specifications that are known to be safe to use in the presence of partial order reduction.
A description of how stuttered states are introduced and of a system of patterns for LTL formulas that are safe to use, despite the fact that they use the next operator, are given. To automatically determine if a formula matches one of the safe patterns, a Prolog based LTL recognizer which we developed is discussed. A listing of the patterns of formulas recognized is given as an appendix