Planning in Nondeterministic Domains under Partial Observability via Symbolic Model Checking