Abstract:

Bounded Model Construction for Monadic Second-Order Logics

Abdelwaheb Ayari and David Basin


The monadic logics M2L 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 phi and a bound k, does there exist a word model for phi of length k. We give a bounded model construction algorithm for M2L that runs in a time exponential in k. For WS1S, we prove a negative result: bounded model construction is as hard as validity checking, ie, 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.