Bounded Model Checking for All Regular Properties

The technique of bounded model checking is extended to the linear time μ-calculus, a temporal logic that can express all monadic second-order properties of ω-words, in other words, all ω-regular languages. Experimental evidence is presented showing that the method can be successfully employed for properties that are hard or impossible to express in the weaker logic LTL that is traditionally used in bounded model checking.