A Hierarchical Task-Network Planner based on Symbolic Model Checking