@InProceedings{cavBMC00.bib,
author = {Ayari, Abdelwaheb and Basin, David},
title = {Bounded Model Construction for Monadic Second-Order
Logics},
booktitle = {12th International Conference on Computer-Aided
Verification (CAV'00)},
pages = {99--113},
year = 2000,
number = 1855,
series = {Lecture Notes in Computer Science},
address = {Chicago, USA},
month = {July},
publisher = {Springer-Verlag},
abstract =
{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.}
}