Planning in Non-Deterministic Domains via Symbolic Model Checking