Planning as model checking for extended goals in non-deterministic Domains