Dealing with incompleteness in automata-based model checking