Weak, strong, and strong cyclic planning via symbolic model checking