{"id":{"repo_id":"rice","oai_identifier":"oai:repository.rice.edu:1911/88419"},"canonical_url":"https://search.dev.ndltd.org/etd/rice/oai:repository.rice.edu:1911/88419","repository":{"repo_id":"rice","name":"Rice University","base_url":"https://repository.rice.edu/server/oai/request"},"display":{"title":"A Constraint-Based Approach to Reactive Task and Motion Planning","abstract":"This thesis presents a novel and scalable approach for Reactive Task and Motion Planning. 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 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 Temporal Property Verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures. Furthermore, the SMT solver 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.","abstract_html":"This thesis presents a novel and scalable approach for Reactive Task and Motion Planning. 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 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 Temporal Property Verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures. Furthermore, the SMT solver 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.","abstract_has_math":false,"creators":["Wang, Yue"],"institution":"Rice University","degree_name":"Master of Science","degree_level":"Masters","degree_discipline":"Engineering","degree_department":null,"school":null,"contributors":[],"advisors":["Chaudhuri, Swarat"],"committee_chairs":[],"committee_members":["Kavraki, Lydia E","Vardi, Moshe Y"],"year":2016,"date_issued":"2016-01-26","date_published":"2016-01-26","updated_at":"2026-07-24T04:10:17Z","subjects":["Constraint-based approaches","Reactive synthesis","Syntax-guided synthesis","Mobile manipulation"],"languages":["eng"],"rights":["Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1911/88419","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Chaudhuri, Swarat"]},{"key":"dc:contributor.committeemember","label":"Committee Member","values":["Kavraki, Lydia E","Vardi, Moshe Y"]},{"key":"dc:creator","label":"Author","values":["Wang, Yue"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2016-02-05T21:46:36Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2016-02-05T21:46:36Z"]},{"key":"dc:date.issued","label":"Date","values":["2016-01-26"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Rice University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Constraint-based approaches","Reactive synthesis","Syntax-guided synthesis","Mobile manipulation"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1911/88419"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["This thesis presents a novel and scalable approach for Reactive Task and Motion Planning. 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 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 Temporal Property Verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures. Furthermore, the SMT solver 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."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["A Constraint-Based Approach to Reactive Task and Motion Planning"]}]}],"canonical_facts":{"dc:contributor.advisor":["Chaudhuri, Swarat"],"dc:contributor.committeemember":["Kavraki, Lydia E","Vardi, Moshe Y"],"dc:creator":["Wang, Yue"],"dc:date.accessioned":["2016-02-05T21:46:36Z"],"dc:date.available":["2016-02-05T21:46:36Z"],"dc:date.issued":["2016-01-26"],"dc:description.abstract":["This thesis presents a novel and scalable approach for Reactive Task and Motion Planning. 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 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 Temporal Property Verification. For efficient policy search, we apply domain-specific heuristics to generalize verification failures. Furthermore, the SMT solver 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."],"dc:format.mimetype":["application/pdf"],"dc:identifier.uri":["https://hdl.handle.net/1911/88419"],"dc:language.iso":["eng"],"dc:rights":["Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder."],"dc:subject":["Constraint-based approaches","Reactive synthesis","Syntax-guided synthesis","Mobile manipulation"],"dc:title":["A Constraint-Based Approach to Reactive Task and Motion Planning"],"dc:type":["Thesis"],"thesis:degree_discipline":["Engineering"],"thesis:degree_level":["Masters"],"thesis:degree_name":["Master of Science"],"thesis:institution_name":["Rice University"]},"updated_at":"2026-07-24T04:10:17Z"}