@inproceedings{camacho-hsdip16-ltl,
  title = {LTL Synthesis for Non-Deterministic Systems on Finite and Infinite Traces},
  author = {Alberto Camacho and Eleni Triantafillou and Christian Muise and Jorge Baier and Sheila A. McIlraith},
  booktitle = {Workshop on Heuristic Search and Domain Independent Planning ({HSDIP}'16)},
  year = {2016},
  url = {http://www.haz.ca/papers/camacho-hsdip16-ltl.pdf},
  keywords = {non-deterministic planning, plan generation},
  abstract={Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of planning with temporally extended goals over both finite and infinite traces where actions can be non-deterministic, and where temporally extended goals are specified in linear temporal logic (LTL). Unlike existing LTL planners, we place no restrictions on our LTL formulae beyond those necessary to distinguish finite from infinite trace interpretations. We realize our planner by translating LTL goals into either (Büchi) alternating or non-deterministic finite state automata, and exploiting a state-of-the-art fully observable non-deterministic planner to compute solutions. The resulting planner is sound and complete. Our system addresses a diverse spectrum of LTL planning problems that to this point had not been solvable using AI planning techniques. We do so while demonstrating competitive performance relative to the state of the art in LTL planning.}
}

{"_id":"Q5T5Ssjvk2ecMiazE","bibbaseid":"camacho-triantafillou-muise-baier-mcilraith-ltlsynthesisfornondeterministicsystemsonfiniteandinfinitetraces-2016","downloads":1,"creationDate":"2016-04-15T17:21:12.248Z","title":"LTL Synthesis for Non-Deterministic Systems on Finite and Infinite Traces","author_short":["Camacho, A.","Triantafillou, E.","Muise, C.","Baier, J.","McIlraith, S. A."],"year":2016,"bibtype":"inproceedings","biburl":"www.haz.ca/publications.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"LTL Synthesis for Non-Deterministic Systems on Finite and Infinite Traces","author":[{"firstnames":["Alberto"],"propositions":[],"lastnames":["Camacho"],"suffixes":[]},{"firstnames":["Eleni"],"propositions":[],"lastnames":["Triantafillou"],"suffixes":[]},{"firstnames":["Christian"],"propositions":[],"lastnames":["Muise"],"suffixes":[]},{"firstnames":["Jorge"],"propositions":[],"lastnames":["Baier"],"suffixes":[]},{"firstnames":["Sheila","A."],"propositions":[],"lastnames":["McIlraith"],"suffixes":[]}],"booktitle":"Workshop on Heuristic Search and Domain Independent Planning (HSDIP'16)","year":"2016","url":"http://www.haz.ca/papers/camacho-hsdip16-ltl.pdf","keywords":"non-deterministic planning, plan generation","abstract":"Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of planning with temporally extended goals over both finite and infinite traces where actions can be non-deterministic, and where temporally extended goals are specified in linear temporal logic (LTL). Unlike existing LTL planners, we place no restrictions on our LTL formulae beyond those necessary to distinguish finite from infinite trace interpretations. We realize our planner by translating LTL goals into either (Büchi) alternating or non-deterministic finite state automata, and exploiting a state-of-the-art fully observable non-deterministic planner to compute solutions. The resulting planner is sound and complete. Our system addresses a diverse spectrum of LTL planning problems that to this point had not been solvable using AI planning techniques. We do so while demonstrating competitive performance relative to the state of the art in LTL planning.","bibtex":"@inproceedings{camacho-hsdip16-ltl,\n title = {LTL Synthesis for Non-Deterministic Systems on Finite and Infinite Traces},\n author = {Alberto Camacho and Eleni Triantafillou and Christian Muise and Jorge Baier and Sheila A. McIlraith},\n booktitle = {Workshop on Heuristic Search and Domain Independent Planning ({HSDIP}'16)},\n year = {2016},\n url = {http://www.haz.ca/papers/camacho-hsdip16-ltl.pdf},\n keywords = {non-deterministic planning, plan generation},\n abstract={Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of planning with temporally extended goals over both finite and infinite traces where actions can be non-deterministic, and where temporally extended goals are specified in linear temporal logic (LTL). Unlike existing LTL planners, we place no restrictions on our LTL formulae beyond those necessary to distinguish finite from infinite trace interpretations. We realize our planner by translating LTL goals into either (Büchi) alternating or non-deterministic finite state automata, and exploiting a state-of-the-art fully observable non-deterministic planner to compute solutions. The resulting planner is sound and complete. Our system addresses a diverse spectrum of LTL planning problems that to this point had not been solvable using AI planning techniques. We do so while demonstrating competitive performance relative to the state of the art in LTL planning.}\n}\n\n","author_short":["Camacho, A.","Triantafillou, E.","Muise, C.","Baier, J.","McIlraith, S. A."],"key":"camacho-hsdip16-ltl","id":"camacho-hsdip16-ltl","bibbaseid":"camacho-triantafillou-muise-baier-mcilraith-ltlsynthesisfornondeterministicsystemsonfiniteandinfinitetraces-2016","role":"author","urls":{"Paper":"http://www.haz.ca/papers/camacho-hsdip16-ltl.pdf"},"keyword":["non-deterministic planning","plan generation"],"metadata":{"authorlinks":{"muise, c":"https://www.haz.ca/academic-publications.html"}}},"search_terms":["ltl","synthesis","non","deterministic","systems","finite","infinite","traces","camacho","triantafillou","muise","baier","mcilraith"],"keywords":["non-deterministic planning","plan generation"],"authorIDs":["f4LpZ8LcDrvDyGuip"],"dataSources":["94txRcb2YKX3ChmqR","DprwGzu9heN5GXy3u"]}