Task and Motion Policy Synthesis as Liveness Games

Task and Motion Policy Synthesis as Liveness Games. Wang, Y., Dantam, N., Chaudhuri, S., & Kavraki, L. In

We present a novel and scalable policy synthesis approach for robotics applications. Rather than producing single-path plans for a static environment, we consider changing environments with uncontrollable agents, where the robot needs a policy to respond correctly in the infinite interaction with the environment. Our approach operates on task and motion domains that combine actions over discrete states with continuous, collision-free paths. We synthesize a task and motion policy by iteratively verifying and searching for a policy candidate. For efficient verification, we employ Satisfiability Modulo Theories (SMT) solvers using a new extension of proof rules for policy verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures, providing stricter constraints on policy candidates. Furthermore, the SMT solver underlying our verification step enables quantitative specifications such as energy limits. We benchmark our policy synthesizer in a mobile manipulation domain, showing that our approach offers better scalability compared to a state-of-the-art robotic synthesis tool in the tested benchmarks and demonstrating order- of-magnitude speedup from our heuristics.

@inproceedings {icaps16-181,
    track    = {Robotics Track},
    title    = {Task and Motion Policy Synthesis as Liveness Games},
    url      = {http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13146},
    author   = {Yue Wang and  Neil Dantam and  Swarat Chaudhuri and  Lydia Kavraki},
    abstract = {We present a novel and scalable policy synthesis approach for robotics applications. Rather than producing single-path plans for a static environment, we consider changing environments with uncontrollable agents, where the robot needs a policy to respond correctly in the infinite interaction with the environment. Our approach operates on task and motion domains that combine actions over discrete states with continuous, collision-free paths. We synthesize a task and motion policy by iteratively verifying and searching for a policy candidate. For efficient verification, we employ Satisfiability Modulo Theories (SMT) solvers using a new extension of proof rules for policy verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures, providing stricter constraints on policy candidates. Furthermore, the SMT solver underlying our verification step enables quantitative specifications such as energy limits. We benchmark our policy synthesizer in a mobile manipulation domain, showing that our approach offers better scalability compared to a state-of-the-art robotic synthesis tool in the tested benchmarks and demonstrating order- of-magnitude speedup from our heuristics.},
    keywords = {formal methods for robot planning and control,robot motion; path; task and mission planning and execution,human-aware planning and execution in human-robot interaction; including safety}
}

Downloads: 2

{"_id":"BPktSxiERPL6Lev2K","bibbaseid":"wang-dantam-chaudhuri-kavraki-taskandmotionpolicysynthesisaslivenessgames","downloads":2,"creationDate":"2016-03-30T13:31:02.287Z","title":"Task and Motion Policy Synthesis as Liveness Games","author_short":["Wang, Y.","Dantam, N.","Chaudhuri, S.","Kavraki, L."],"year":null,"bibtype":"inproceedings","biburl":"icaps16.icaps-conference.org/papers.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","track":"Robotics Track","title":"Task and Motion Policy Synthesis as Liveness Games","url":"http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13146","author":[{"firstnames":["Yue"],"propositions":[],"lastnames":["Wang"],"suffixes":[]},{"firstnames":["Neil"],"propositions":[],"lastnames":["Dantam"],"suffixes":[]},{"firstnames":["Swarat"],"propositions":[],"lastnames":["Chaudhuri"],"suffixes":[]},{"firstnames":["Lydia"],"propositions":[],"lastnames":["Kavraki"],"suffixes":[]}],"abstract":"We present a novel and scalable policy synthesis approach for robotics applications. Rather than producing single-path plans for a static environment, we consider changing environments with uncontrollable agents, where the robot needs a policy to respond correctly in the infinite interaction with the environment. Our approach operates on task and motion domains that combine actions over discrete states with continuous, collision-free paths. We synthesize a task and motion policy by iteratively verifying and searching for a policy candidate. For efficient verification, we employ Satisfiability Modulo Theories (SMT) solvers using a new extension of proof rules for policy verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures, providing stricter constraints on policy candidates. Furthermore, the SMT solver underlying our verification step enables quantitative specifications such as energy limits. We benchmark our policy synthesizer in a mobile manipulation domain, showing that our approach offers better scalability compared to a state-of-the-art robotic synthesis tool in the tested benchmarks and demonstrating order- of-magnitude speedup from our heuristics.","keywords":"formal methods for robot planning and control,robot motion; path; task and mission planning and execution,human-aware planning and execution in human-robot interaction; including safety","bibtex":"@inproceedings {icaps16-181,\r\n track = {Robotics Track},\r\n title = {Task and Motion Policy Synthesis as Liveness Games},\r\n url = {http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13146},\r\n author = {Yue Wang and Neil Dantam and Swarat Chaudhuri and Lydia Kavraki},\r\n abstract = {We present a novel and scalable policy synthesis approach for robotics applications. Rather than producing single-path plans for a static environment, we consider changing environments with uncontrollable agents, where the robot needs a policy to respond correctly in the infinite interaction with the environment. Our approach operates on task and motion domains that combine actions over discrete states with continuous, collision-free paths. We synthesize a task and motion policy by iteratively verifying and searching for a policy candidate. For efficient verification, we employ Satisfiability Modulo Theories (SMT) solvers using a new extension of proof rules for policy verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures, providing stricter constraints on policy candidates. Furthermore, the SMT solver underlying our verification step enables quantitative specifications such as energy limits. We benchmark our policy synthesizer in a mobile manipulation domain, showing that our approach offers better scalability compared to a state-of-the-art robotic synthesis tool in the tested benchmarks and demonstrating order- of-magnitude speedup from our heuristics.},\r\n keywords = {formal methods for robot planning and control,robot motion; path; task and mission planning and execution,human-aware planning and execution in human-robot interaction; including safety}\r\n}\r\n\r\n","author_short":["Wang, Y.","Dantam, N.","Chaudhuri, S.","Kavraki, L."],"key":"icaps16-181","id":"icaps16-181","bibbaseid":"wang-dantam-chaudhuri-kavraki-taskandmotionpolicysynthesisaslivenessgames","role":"author","urls":{"Paper":"http://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13146"},"keyword":["formal methods for robot planning and control","robot motion; path; task and mission planning and execution","human-aware planning and execution in human-robot interaction; including safety"],"metadata":{"authorlinks":{}},"downloads":2,"html":""},"search_terms":["task","motion","policy","synthesis","liveness","games","wang","dantam","chaudhuri","kavraki"],"keywords":["formal methods for robot planning and control","robot motion; path; task and mission planning and execution","human-aware planning and execution in human-robot interaction; including safety"],"authorIDs":[],"dataSources":["iMkx859KiXcegwsin","EZtZjCTnxcdTTyeij"]}