{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T00:00:18Z","timestamp":1743120018238,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030286187"},{"type":"electronic","value":"9783030286194"}],"license":[{"start":{"date-parts":[[2019,11,28]],"date-time":"2019-11-28T00:00:00Z","timestamp":1574899200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-28619-4_57","type":"book-chapter","created":{"date-parts":[[2019,11,28]],"date-time":"2019-11-28T00:04:15Z","timestamp":1574899455000},"page":"827-842","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parallelizing Synthesis from Temporal Logic Specifications by Identifying Equicontrollable States"],"prefix":"10.1007","author":[{"given":"Sumanth","family":"Dathathri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ioannis","family":"Filippidis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard M.","family":"Murray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,11,28]]},"reference":[{"key":"57_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Moarref, S., Topcu, U.: Compositional synthesis with parametric reactive controllers. In: Proceedings of HSCC, pp. 215\u2013224 (2016)","DOI":"10.1145\/2883817.2883842"},{"key":"57_CR2","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78, 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"9","key":"57_CR3","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"issue":"1","key":"57_CR4","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/S0304-3975(96)00228-9","volume":"178","author":"A Browne","year":"1997","unstructured":"Browne, A., Clarke, E., Jha, S., Long, D., Marrero, W.: An improved algorithm for the evaluation of fixpoint expressions. Theor. Comput. Sci. 178(1), 237\u2013255 (1997)","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"57_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"57_CR6","first-page":"205","volume":"40","author":"RE Bryant","year":"1991","unstructured":"Bryant, R.E.: On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. TOC 40(2), 205\u2013213 (1991)","journal-title":"TOC"},{"key":"57_CR7","doi-asserted-by":"crossref","unstructured":"Chinchali, S., Livingston, S.C., Topcu, U., Burdick, J.W., Murray, R.M.: Towards formal synthesis of reactive controllers for dexterous robotic manipulation. In: Proceedings of ICRA, pp. 5183\u20135189 (2012)","DOI":"10.1109\/ICRA.2012.6225257"},{"key":"57_CR8","doi-asserted-by":"crossref","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: SPLIT: a compositional LTL verifier. In: CAV, pp. 558\u2013561 (2010)","DOI":"10.1007\/978-3-642-14295-6_47"},{"key":"57_CR9","doi-asserted-by":"crossref","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y., Zuck, L.D., Kisyova, K.I.: Parallelizing a symbolic compositional model-checking algorithm. In: Proceedings of HVC, pp. 46\u201359 (2010)","DOI":"10.1007\/978-3-642-19583-9_9"},{"key":"57_CR10","doi-asserted-by":"crossref","unstructured":"Dathathri, S., Murray, R.M.: Decomposing GR(1) games with singleton liveness guarantees for efficient synthesis. In: Proceedings of CDC, pp. 911\u2013917 (2017)","DOI":"10.1109\/CDC.2017.8263775"},{"key":"57_CR11","doi-asserted-by":"crossref","unstructured":"DeCastro, J.A., Alonso-Mora, J., Raman, V., Rus, D., Kress-Gazit, H.: Collision-free reactive mission and motion planning for multi-robot systems. In: Proceedings of ISRR, pp. 459\u2013476 (2015)","DOI":"10.1007\/978-3-319-51532-8_28"},{"key":"57_CR12","doi-asserted-by":"crossref","unstructured":"Ehlers, R., Raman, V.: Slugs: extensible GR(1) synthesis. In: Proceedings of CAV, pp. 333\u2013339 (2016)","DOI":"10.1007\/978-3-319-41540-6_18"},{"key":"57_CR13","unstructured":"Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional mu-calculus. In: IEEE Computer Society Press LICS, pp. 267\u2013278 (1986)"},{"key":"57_CR14","doi-asserted-by":"crossref","unstructured":"Filippidis, I., Dathathri, S., Livingston, S.C., Ozay, N., Murray, R.M.: Control design for hybrid systems with TuLiP: the temporal logic planning toolbox. In: Proceedings of CCA, pp. 1030\u20131041 (2016)","DOI":"10.1109\/CCA.2016.7587949"},{"key":"57_CR15","doi-asserted-by":"crossref","unstructured":"Filippidis, I., Murray, R.M., Holzmann, G.J.: A multi-paradigm language for reactive synthesis. In: 4$$^{th}$$ work. on synthesis, SYNT, pp. 73\u201397 (2015)","DOI":"10.4204\/EPTCS.202.6"},{"key":"57_CR16","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.ic.2005.01.006","volume":"200","author":"Y Kesten","year":"2005","unstructured":"Kesten, Y., Piterman, N., Pnueli, A.: Bridging the gap between fair simulation and trace inclusion. Inf. Comput. 200, 35\u201361 (2005)","journal-title":"Inf. Comput."},{"key":"57_CR17","doi-asserted-by":"crossref","unstructured":"Klein, U., Pnueli, A.: Revisiting synthesis of GR(1) specifications. In: Proceedings of HVC, pp. 161\u2013181 (2010)","DOI":"10.1007\/978-3-642-19583-9_16"},{"key":"57_CR18","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Where\u2019s Waldo? sensor-based temporal logic motion planning. In: Proceedings of ICRA, pp. 3116\u20133121 (2007)","DOI":"10.1109\/ROBOT.2007.363946"},{"issue":"3","key":"57_CR19","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. TOPLAS 16(3), 872\u2013923 (1994)","journal-title":"TOPLAS"},{"key":"57_CR20","unstructured":"Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002)"},{"key":"57_CR21","doi-asserted-by":"crossref","unstructured":"Majumdar, R.: Robots at the edge of the cloud. In: Proceedings of TACAS, pp. 3\u201313 (2016)","DOI":"10.1007\/978-3-662-49674-9_1"},{"key":"57_CR22","doi-asserted-by":"crossref","unstructured":"Maniatopoulos, S., Schillinger, P., Pong, V., Conner, D.C., Kress-Gazit, H.: Reactive high-level behavior synthesis for an Atlas humanoid robot. In: Proceedings of ICRA, pp. 4192\u20134199 (2016)","DOI":"10.1109\/ICRA.2016.7487613"},{"key":"57_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of PODC, pp. 377\u2013408 (1990)","DOI":"10.1145\/93385.93442"},{"key":"57_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"57_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"57_CR26","unstructured":"Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of ICCAD, pp. 42\u201347 (1993)"},{"key":"57_CR27","unstructured":"van Dijk, T., Laarman, A., van\u00a0de Pol, J.: Multi-core BDD operations for symbolic reachability. ENTCS (PDMC\u201912) 296, 127\u2013143 (2013)"},{"key":"57_CR28","doi-asserted-by":"crossref","unstructured":"Wolff, E.M., Murray, R.M.: Optimal control of nonlinear systems with temporal logic specifications. In: Proceedings of ISRR, pp. 21\u201337 (2013)","DOI":"10.1007\/978-3-319-28872-7_2"}],"container-title":["Springer Proceedings in Advanced Robotics","Robotics Research"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-28619-4_57","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T21:25:43Z","timestamp":1586467543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-28619-4_57"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,28]]},"ISBN":["9783030286187","9783030286194"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-28619-4_57","relation":{},"ISSN":["2511-1256","2511-1264"],"issn-type":[{"type":"print","value":"2511-1256"},{"type":"electronic","value":"2511-1264"}],"subject":[],"published":{"date-parts":[[2019,11,28]]},"assertion":[{"value":"28 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}