Bounded model construction for monadic second-order logics

Abstract

The monadic logics M2L-STR and WS1S have been successfully used for verification, although they are nonelementary decidable. Motivated by ideas from bounded model checking, we investigate procedures for bounded model construction for these logics. The problem is, given a formula ϕ and a bound k, does there exist a word model for ϕ of length k. We give a bounded model construction algorithm for M2L- STR that runs in a time exponential in k. For WS1S, we prove a negative result: bounded model construction is as hard as validity checking, i.e., it is nonelementary. From this, negative results for other monadic logics, such as S1S, follow. We present too preliminary tests using a SAT-based implementation of bounded model construction; for certain problem classes it can find counter-examples substantially faster than automata-based decision procedures.