{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/50573"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/50573","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Optimal planning with temporal logic specifications","abstract":"Most of the current uninhabitated Aerial Vehicles (UAVs) are individually monitored, commanded and controlled by several operators of different expertise. However, looking forward, there has been a recent interest in multiple-UAV systems, in which the system is only provided with the high-level goals and constraints, called the \"mission specifications,\" and asked to navigate the UAVs such that the mission specifications are fulfilled. A crucial part in designing such multiple-UAV systems is the development of coordination and planning algorithms that, given a set of high-level mission specifications as input, can synthesize provably correct and possibly optimal schedules for each of the UAVs. This thesis studies optimal planning problems in a multiple-UAV mission planning setting, where the mission specifications are given in formal languages. The problem is posed as a novel variant of the Vehicle Routing Problem (VRP), in which temporal logics and process algebra are utilized to represent a large class of mission specifications in a systematic way. The thesis is structured in two parts. In the first part, two temporal logics that are remarkably close to the natural language, namely the linear temporal logic LTL-x and the metric temporal logic (MTL), are considered for specification of a large class of temporal and logical constraints in VRPs. Mixed-integer linear programming based algorithms, which solve these variants of the VRP to optimality, are presented. In the second part, process algebra is introduced and used as a candidate for the same purpose.","abstract_html":"Most of the current uninhabitated Aerial Vehicles (UAVs) are individually monitored, commanded and controlled by several operators of different expertise. However, looking forward, there has been a recent interest in multiple-UAV systems, in which the system is only provided with the high-level goals and constraints, called the "mission specifications," and asked to navigate the UAVs such that the mission specifications are fulfilled. A crucial part in designing such multiple-UAV systems is the development of coordination and planning algorithms that, given a set of high-level mission specifications as input, can synthesize provably correct and possibly optimal schedules for each of the UAVs. This thesis studies optimal planning problems in a multiple-UAV mission planning setting, where the mission specifications are given in formal languages. The problem is posed as a novel variant of the Vehicle Routing Problem (VRP), in which temporal logics and process algebra are utilized to represent a large class of mission specifications in a systematic way. The thesis is structured in two parts. In the first part, two temporal logics that are remarkably close to the natural language, namely the linear temporal logic LTL-x and the metric temporal logic (MTL), are considered for specification of a large class of temporal and logical constraints in VRPs. Mixed-integer linear programming based algorithms, which solve these variants of the VRP to optimality, are presented. In the second part, process algebra is introduced and used as a candidate for the same purpose.","abstract_has_math":false,"creators":["Karaman, Sertac"],"institution":"Massachusetts Institute of Technology","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Dept. of Mechanical Engineering.","school":null,"contributors":[],"advisors":["Emilio Frazzoli."],"committee_chairs":[],"committee_members":[],"year":2009,"date_issued":"2009","date_published":"2009","updated_at":"2026-07-22T22:22:06Z","subjects":["Mechanical Engineering."],"languages":["eng"],"rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/1721.1/50573","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Emilio Frazzoli."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Dept. of Mechanical Engineering."]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Dept. of Mechanical Engineering."]},{"key":"dc:creator","label":"Author","values":["Karaman, Sertac"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2010-01-07T20:55:06Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2010-01-07T20:55:06Z"]},{"key":"dc:date.issued","label":"Date","values":["2009"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Mechanical Engineering."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["http://hdl.handle.net/1721.1/50573"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Mechanical Engineering, 2009.","Includes bibliographical references (p. 117-121)."]},{"key":"dc:description.abstract","label":"Abstract","values":["Most of the current uninhabitated Aerial Vehicles (UAVs) are individually monitored, commanded and controlled by several operators of different expertise. However, looking forward, there has been a recent interest in multiple-UAV systems, in which the system is only provided with the high-level goals and constraints, called the \"mission specifications,\" and asked to navigate the UAVs such that the mission specifications are fulfilled. A crucial part in designing such multiple-UAV systems is the development of coordination and planning algorithms that, given a set of high-level mission specifications as input, can synthesize provably correct and possibly optimal schedules for each of the UAVs. This thesis studies optimal planning problems in a multiple-UAV mission planning setting, where the mission specifications are given in formal languages. The problem is posed as a novel variant of the Vehicle Routing Problem (VRP), in which temporal logics and process algebra are utilized to represent a large class of mission specifications in a systematic way. The thesis is structured in two parts. In the first part, two temporal logics that are remarkably close to the natural language, namely the linear temporal logic LTL-x and the metric temporal logic (MTL), are considered for specification of a large class of temporal and logical constraints in VRPs. Mixed-integer linear programming based algorithms, which solve these variants of the VRP to optimality, are presented. In the second part, process algebra is introduced and used as a candidate for the same purpose.","(cont.) A tree search based anytime algorithm is given; this algorithm is guarranteed to find a best-first feasible solution in polynomial time and improve it to an optimal one in finite time."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:title","label":"Title","values":["Optimal planning with temporal logic specifications"]}]}],"canonical_facts":{"dc:contributor.advisor":["Emilio Frazzoli."],"dc:contributor.department":["Massachusetts Institute of Technology. Dept. of Mechanical Engineering."],"dc:contributor.other":["Massachusetts Institute of Technology. Dept. of Mechanical Engineering."],"dc:creator":["Karaman, Sertac"],"dc:date.accessioned":["2010-01-07T20:55:06Z"],"dc:date.available":["2010-01-07T20:55:06Z"],"dc:date.issued":["2009"],"dc:description":["Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Mechanical Engineering, 2009.","Includes bibliographical references (p. 117-121)."],"dc:description.abstract":["Most of the current uninhabitated Aerial Vehicles (UAVs) are individually monitored, commanded and controlled by several operators of different expertise. However, looking forward, there has been a recent interest in multiple-UAV systems, in which the system is only provided with the high-level goals and constraints, called the \"mission specifications,\" and asked to navigate the UAVs such that the mission specifications are fulfilled. A crucial part in designing such multiple-UAV systems is the development of coordination and planning algorithms that, given a set of high-level mission specifications as input, can synthesize provably correct and possibly optimal schedules for each of the UAVs. This thesis studies optimal planning problems in a multiple-UAV mission planning setting, where the mission specifications are given in formal languages. The problem is posed as a novel variant of the Vehicle Routing Problem (VRP), in which temporal logics and process algebra are utilized to represent a large class of mission specifications in a systematic way. The thesis is structured in two parts. In the first part, two temporal logics that are remarkably close to the natural language, namely the linear temporal logic LTL-x and the metric temporal logic (MTL), are considered for specification of a large class of temporal and logical constraints in VRPs. Mixed-integer linear programming based algorithms, which solve these variants of the VRP to optimality, are presented. In the second part, process algebra is introduced and used as a candidate for the same purpose.","(cont.) A tree search based anytime algorithm is given; this algorithm is guarranteed to find a best-first feasible solution in polynomial time and improve it to an optimal one in finite time."],"dc:description.degree":["S.M."],"dc:identifier.uri":["http://hdl.handle.net/1721.1/50573"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Mechanical Engineering."],"dc:title":["Optimal planning with temporal logic specifications"],"dc:type":["Thesis"]},"updated_at":"2026-07-22T22:22:06Z"}