@inproceedings{camacho-genplan-17,
  title = {Bridging the Gap Between LTL Synthesis and Automated Planning},
  author = {Alberto Camacho and Jorge Baier and Christian Muise and Sheila A. McIlraith},
  booktitle = {Workshop on Generalized Planning ({GenPlan}'17)},
  year = {2017},
  url = {http://www.cs.toronto.edu/~sheila/publications/cam-etal-genplan17.pdf},
  abstract={Linear Temporal Logic (LTL) synthesis can be understood as the problem of building a controller that defines a winning strategy, for a two-player game against the environment, where the objective is to satisfy a given LTL formula. It is an important problem with applications in software synthesis, including controller synthesis. Recent work has explored the close connection between automated planning and LTL synthesis but has not provided a full mapping between the two problems nor have its practical implications been explored. In this paper we establish the correspondence between LTL synthesis and fully observable non-deterministic (FOND) planning. We also provide the first explicit compilation that translates an LTL synthesis problem to a FOND problem. Experiments with state-of-the-art LTL FOND and synthesis solvers show automated planning to be a viable and effective tool for highly structured LTL synthesis problems.}
}

{"_id":"sQJHQR7SLscNQBPTz","bibbaseid":"camacho-baier-muise-mcilraith-bridgingthegapbetweenltlsynthesisandautomatedplanning-2017","downloads":8,"creationDate":"2017-05-26T21:04:55.372Z","title":"Bridging the Gap Between LTL Synthesis and Automated Planning","author_short":["Camacho, A.","Baier, J.","Muise, C.","McIlraith, S. A."],"year":2017,"bibtype":"inproceedings","biburl":"www.haz.ca/publications.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Bridging the Gap Between LTL Synthesis and Automated Planning","author":[{"firstnames":["Alberto"],"propositions":[],"lastnames":["Camacho"],"suffixes":[]},{"firstnames":["Jorge"],"propositions":[],"lastnames":["Baier"],"suffixes":[]},{"firstnames":["Christian"],"propositions":[],"lastnames":["Muise"],"suffixes":[]},{"firstnames":["Sheila","A."],"propositions":[],"lastnames":["McIlraith"],"suffixes":[]}],"booktitle":"Workshop on Generalized Planning (GenPlan'17)","year":"2017","url":"http://www.cs.toronto.edu/~sheila/publications/cam-etal-genplan17.pdf","abstract":"Linear Temporal Logic (LTL) synthesis can be understood as the problem of building a controller that defines a winning strategy, for a two-player game against the environment, where the objective is to satisfy a given LTL formula. It is an important problem with applications in software synthesis, including controller synthesis. Recent work has explored the close connection between automated planning and LTL synthesis but has not provided a full mapping between the two problems nor have its practical implications been explored. In this paper we establish the correspondence between LTL synthesis and fully observable non-deterministic (FOND) planning. We also provide the first explicit compilation that translates an LTL synthesis problem to a FOND problem. Experiments with state-of-the-art LTL FOND and synthesis solvers show automated planning to be a viable and effective tool for highly structured LTL synthesis problems.","bibtex":"@inproceedings{camacho-genplan-17,\n title = {Bridging the Gap Between LTL Synthesis and Automated Planning},\n author = {Alberto Camacho and Jorge Baier and Christian Muise and Sheila A. McIlraith},\n booktitle = {Workshop on Generalized Planning ({GenPlan}'17)},\n year = {2017},\n url = {http://www.cs.toronto.edu/~sheila/publications/cam-etal-genplan17.pdf},\n abstract={Linear Temporal Logic (LTL) synthesis can be understood as the problem of building a controller that defines a winning strategy, for a two-player game against the environment, where the objective is to satisfy a given LTL formula. It is an important problem with applications in software synthesis, including controller synthesis. Recent work has explored the close connection between automated planning and LTL synthesis but has not provided a full mapping between the two problems nor have its practical implications been explored. In this paper we establish the correspondence between LTL synthesis and fully observable non-deterministic (FOND) planning. We also provide the first explicit compilation that translates an LTL synthesis problem to a FOND problem. Experiments with state-of-the-art LTL FOND and synthesis solvers show automated planning to be a viable and effective tool for highly structured LTL synthesis problems.}\n}\n\n\n","author_short":["Camacho, A.","Baier, J.","Muise, C.","McIlraith, S. A."],"key":"camacho-genplan-17","id":"camacho-genplan-17","bibbaseid":"camacho-baier-muise-mcilraith-bridgingthegapbetweenltlsynthesisandautomatedplanning-2017","role":"author","urls":{"Paper":"http://www.cs.toronto.edu/~sheila/publications/cam-etal-genplan17.pdf"},"metadata":{"authorlinks":{"camacho, a":"http://www.albertocamacho.com/","mcilraith, s":"https://www.cs.toronto.edu/~sheila/publications/","muise, c":"https://haz.ca/academic-publications.html"}},"downloads":8},"search_terms":["bridging","gap","between","ltl","synthesis","automated","planning","camacho","baier","muise","mcilraith"],"keywords":[],"authorIDs":["2JP7Eg9bhybNpzYiR","3XTrQJhM6WgBbiDbs","3ZsuB8kFuBazYSYay","3aQBFJkJYCcndwCjR","3b3gnNFqBHiteKXs2","3hYo439g2MuAaCX6e","3wSJLXJ9XuZ2mDm2H","49zg6n33JhWCCjH4G","4QhCAt6rJiarXgGTG","4zKMDaLdYLdgGQChe","5456dccd8b01c81930000008","5456e0ad8b01c8193000001d","5456f48b8b01c819300000ab","59f3b72dee99a95d4d00003b","5Eidhk5inwxxe7JGk","5de6d3d8abd988de010000ca","5de8f2ff978afbdf01000180","5de9e8f29f521ddf010000f4","5dea039cfac96fde010000ad","5dea0c58fac96fde01000141","5deb0462a31587de010000a3","5df13ef7630a9ee0010000b3","5df2ea54b91ab0de010000ea","5df52514ea1457de01000126","5df7e072dc100cde0100014e","5df993a1c4ada8de01000019","5df99645c4ada8de0100003b","5dfaab875481b4de0100001d","5dfb881fc2820bdf010001a1","5dfe6b5e4e3a44de0100001f","5dff511bddf837de01000075","5e03673eb1544ef201000082","5e044e70705486df010000b8","5e046c906ef264df010000b9","5e0602f7e95bcdde0100005b","5e0623ba8e1565f2010000cf","5e0b2662fc92e9de01000023","5e10276e2ef76bdf0100009f","5e129793551229df010000b6","5e12ae713f181ade01000085","5e136ddaf16095df0100010c","5e15ebbcefa1cddf0100005f","5e160321efa1cddf01000277","5e162befdf1bb4de01000116","5e16303adf1bb4de01000195","5e175171883585df010001f5","5e185337809b84f20100000a","5e194fb886b4aade010000f1","5e1c6302e556c6de010001e8","5e1d8ada3a6d8cde0100011c","5e1dc2b98d71ddde010000f2","5e1e7705ce9ed9de0100012a","5e1eadd6bedb58de01000124","5e1f7406e8f5ddde01000229","5e2093efbdda1fde0100003c","5e21b52196aea7de010000a0","5e25b773b57878de010001e1","5e26328524c8a6de0100006d","5e270f9cf51e02de0100005a","5e2723abf51e02de010001fb","5e272ebd557b88de010000b6","5e2784f755fc50df01000004","5e27b36b28f7a6de01000151","5e28be096acacbdf010000d4","5e2b334a27ed83df01000123","5e2dae33732e89de0100005c","5e2e0116524f94de0100005d","5e2e2abccc9e90e4010000fc","5e2ea3edb84405df01000035","5e3081b4cb949bdf01000044","5e324da4e45eb5df010000d5","5e326f1a5633c9de010000b0","5e3449e70c807ede01000132","5e3555a950cde4de0100000c","5e3627ac1727e7df010000c2","5e37c25d56571fde0100003d","5e380024918d4ede01000092","5e386d181f8af9e00100009b","5e3874ed1f8af9e001000122","5e390326dc5b8ade010000ac","5e3b054855f0f2df0100017f","5e3c31bf34cd37de01000126","5e3c5333c798e0de01000129","5e3ec74c86a596de0100000b","5e3ffc1d17f17dde01000002","5e3ffd7017f17dde01000014","5e40b576019547df010000c0","5e41b0910b4861de01000111","5e42164870cecede01000048","5e441c71fdc393de01000118","5e446fd5084293df010000fd","5e44bf6a7759a7df0100007c","5e4628077f6322df01000042","5e4aa2eab70966df0100029f","5e4c5496271596df010000c6","5e4c93785cc521f2010000e0","5e4cec0e3e28aede0100012b","5e4d64b108a8e5de01000031","5e4ea00e64b624de01000072","5e4f53598a3535f3010000cd","5e4f7499a01931de010000b6","5e50202c933046de01000185","5e503b938c3a2cde0100013d","5e514743fe5af9df01000091","5e535d7e45815bf20100006c","5e53f9acd26e87df010001df","5e55431aca58a8df0100019a","5e556ca4e11ab9df01000032","5e55af2b7d0846de010000c4","5e56d52696127bde0100020e","5e5a1adc3557f5df010000c2","5e5a5d62b034a8df0100001b","5e5c3af568f281de01000023","5e5c3b1e68f281de01000026","5e5d6d8b0b73f6de01000003","5e5e62255f9e7bee010001bb","5e5e9d8bc0a53dde01000251","5e5eab682fd1fade010000e2","5e5ee78ccc2eefde01000085","5e601cf3c064fcde010001dd","5e65c1b1d92058de010000e3","5e665cdd46e828de0100014d","5e66fa7685689bf30100010e","5e670701511133df0100006d","5e68f51f1a389bdf0100045c","5rfKneErnpvH8A9jA","5yN3GPwHiapRhtuj9","6C5wfAZryB8LaY2PJ","6RJeJwCaTdt9z5nYv","6Z2RfBdBMBFMMobst","6jNNJBuk6HAtcnEvy","6vPX7dp4BL2qMjx2i","7AuroeLTMFPfJCoc5","7bxyKKMGnHxEQh3cj","7deQZsScCfPeKMrqy","8j3GdPnZ34L7MwaRH","9jPSyMaccQATNQzFR","ATNoaRSndJwiMQonw","AtaDzKGXz9bfKWfab","BELXag98NmsXoYgsH","BiCJ3yKjnhWp5CCMC","CBLksFoEERH5GZA5T","CEHomL2HupdANcjHm","CeALjMgBHZmr9SzLQ","CzTmxSkSkem3essqH","D7u3CRvfQdZb2Nsvb","DPH6F3udnr4WBuFRg","DTvS4QdpaPswfTdKK","Dcjwdot9d5rJFoLNW","EZxoX4JE4byz9dLBS","FE3yhyj5fmmfLuJXZ","FTTuMEgm3yh9QH7pw","FfGeNRF9QvLSRujvc","GKYqrPg3uj7nu7nbt","GQWTrxJz3HKdJcAEM","GfiiL4m6PWnSrb5pM","GvvCbq8Y4n9QqTySC","H5crAWCHh6CtutSp3","HF25KvZDEBf5Nvp8x","HTN44dpu77wAWF8HE","HhKYdEPpCZAmKPPQc","HwSBgNFgx9YdcbTkD","J5FZeQWmDd6p96K8P","J9Cn8pzsqP9mpr6xy","JDoXnkWb7QmkjpPqn","JGfakYisbgxjaayRF","JJ4YdoB6PqRk2mbBH","JjhEWvgeq8Qx6LZof","Jw793vyTqsyX5daKz","KZfCyiyswf4sBtGjP","KgBg49s7JcYbLSctC","KpA6noWknYigzPP4i","KwLm5LfL8LpgKk8XJ","Lk4oC9xJyhagKJyo6","LwbwhDPiGy5gvQipm","MroboN368do5mezgH","NAb7GKwczGhpSRtaE","NAyJtGS6K2wBWJMx2","NBcXbcFrQdwCtndaF","NJYBJe35TWp5FARRc","Ni37kLLmf4zgkdNFZ","PFRbwQewWEdMfk4Mk","PZYJkWyWoKeykNsHr","QvNgkQwXWMDTxciYq","QwjvvLtMervWzsLig","RStoeQpfqvDsMSLzJ","S6JseZ2prMTKs24ym","SLJpkXgMzHPLEP33v","SPGedFjeWXsYiB6tq","T9PWjMkNwX9WQ5frZ","TcNBkSpMyeu2oxw5A","TrWgLJWQbSjbuF2bq","TuqvMAPdZhcxfZKp7","WAx35JxHCScRCfQYK","WKpwMkNYj2iNsJ48r","WMHiPYnuEnrhKxJWi","WiXjNSHmtpmkHsPYF","Wipe7PE2hMCo9rb5r","WqZpp9fP47artme8L","WvNTfrm4CkuAz6kh9","XCnXFqMPKPFkRq2kj","XDyEccztzCgSrH8JK","XELkWriNsABzHMyaw","XEMAfXz5wSaaLnBkk","YYXt22tWnAnS4ohf4","YYzBhJWRGjiEKRDnZ","Yo9NwQNbXRfSjd5LR","ZgeG2ZjGwAuPqqEmA","Zpzs3SDfCjG7mJAEC","ZysMM8RRSrhEZt4rm","a7KzaH4ok4HAJxnyP","aXBRouHw2x2TwqbuE","ah2FNqZqgqkMf7rno","aijWPoggdP77wxPuf","axB6kamRvmWu5vw6X","b6ZAdn6ZpgQcDuejh","bNHECCPaQAsthaP2z","cavuN3YH45oms9mKy","cgdaZmm5NDtBmBJcL","crArqS5DKyENjHyEF","dBkxSxaYwPmKXxEg8","dJyb7wbihKdDzgkGr","dSvyDxvHdpJ3uQRZS","dXrbumWfb7fR9Kak8","emJa7LZmACzm5bbpv","esY7FSKsHpLphjhKg","f4LpZ8LcDrvDyGuip","fZgBEq2CFLY5oCbhJ","g2oQsrCb47Nfxjnes","goA6xywLeZi8P9Z3N","goc5YRXzjuZMrzKik","grCkvcC8cTZqJzGKu","hfmvhLcJ6rSarhyHM","hnF3mFjXA6XYLLhgh","htW24MBmx67vY4Dky","htrNC4rPDzh6zfTLS","iEMJPovEGF7jk6vBD","iWkYLX2HSxaiwbphr","j6foRqya6fLiniZC3","j9wxxJ9nPog3bHXaY","jArTXYwhaXss62KJk","jBLcydKWE5xxJKofs","jDsmsaB2wJpvPgxE4","jQ6CLx98WT9tg54oT","jtKbSfonQ5YmGvpfh","jvXSefynz5Ba7gqX2","kHSR5D3QYy2f3iKFf","kSfpomb2i9SWgtiBN","kYGNCbRdzB9CHBr5s","karY5HSFumjds5vuz","kx2M4GyrQDBEqRT4q","m6X7Yg32T74Fxxn2d","mDT7qYTqNpZo4tXcj","mZRqmrrWcFXhvyhAi","mwfq6DupsNxXZhwFK","n5nsNDT3PrjBRrmw6","n8ip3yxvw6k38QpZL","nhPAKwaJ3yD2ihuqD","nvsBeFCxyzjQRGPSi","o39uWBuFedviW43Cw","ouiBqDxCbBeEAQCeW","ow6c7LGcrn2X6iWQd","pRtcYGMaZMG8GTaSz","paM4BdJgmXhvmhNf8","qwPzsaveEtEvDqBPs","rhiD5xJXuoWPMReit","rkDRNeSmuJeNswCfv","sYAXaopmi2wx9uPsF","t7Mi3Geoz9C8Aibas","tMexbXp8PoEkbZnrv","tRLzqBJWc3TYzBYox","tmHrh8yBFTwMrLukn","uHSZiLRwEgNpbmmRw","uxproQToHm4wEZeph","vCzpvySfmJ5w7kMBh","vReYR7kzq7n4RR9Ng","wGWyTtcLspnfJaLeT","wfhA6qG7fcni6LQuw","wsyXZn5iRF2dciL8t","x6aX8g9rWCY5wzyW2","xTKWRxJPtd5N9aKTq","xW8eSNRWi7bXhQuHC","xZ6wRPENk64YNgMr7","xm2sosMHyKsPj85Pb","yEypGxYJaM52ipscR","yQ8buY4mGRZGmLKte","ybLsHWfLgzQZAQ5WE","zSHM8azk4tdTPDvou","zsNPuARLzosfgmFwd","zzk9ihDtxJrpejbzN"],"dataSources":["2LLKDfkxMDdABm58M","euD7cPywCk5gX9zDY","DprwGzu9heN5GXy3u","hqqbBi3M3BaCY6ivH","optQ3PYGE2PxhriFJ","T3oedZczBnZ2Y6GvJ","jHtiDocCziH83gWEu","Jwuh2BtHasSBPk4uf","FAyKHaeKDYM4aGJk2"]}