{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,25]],"date-time":"2025-11-25T06:51:09Z","timestamp":1764053469925,"version":"3.41.0"},"reference-count":70,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,9]]},"DOI":"10.1109\/cca.2016.7587949","type":"proceedings-article","created":{"date-parts":[[2016,10,20]],"date-time":"2016-10-20T20:50:06Z","timestamp":1476996606000},"page":"1030-1041","source":"Crossref","is-referenced-by-count":56,"title":["Control design for hybrid systems with TuLiP: The Temporal Logic Planning toolbox"],"prefix":"10.1109","author":[{"given":"Ioannis","family":"Filippidis","sequence":"first","affiliation":[]},{"given":"Sumanth","family":"Dathathri","sequence":"additional","affiliation":[]},{"given":"Scott C.","family":"Livingston","sequence":"additional","affiliation":[]},{"given":"Necmiye","family":"Ozay","sequence":"additional","affiliation":[]},{"given":"Richard M.","family":"Murray","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_49"},{"journal-title":"2010-2016","article-title":"tulip: The temporal logic planning toolbox (Python package)","year":"0","key":"ref39"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"11","DOI":"10.25080\/TCWV9851","article-title":"Exploring network structure, dynamics, and function using NetworkX","author":"hagberg","year":"2008","journal-title":"SciPy"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1515\/9781400882618-006"},{"key":"ref32","article-title":"Miscellany","author":"lamport","year":"1991","journal-title":"note sent to TLA mailing list"},{"key":"ref31","article-title":"Formalizing synthesis in TLA+","author":"filippidis","year":"2016","journal-title":"Caltech Tech Rep CaltechCDSTR 2016 004"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/32.464544"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5_15"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44618-4_33"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1955.tb03788.x"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2006.886494"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2010.118"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"ref28","first-page":"583","article-title":"Logical specifications of infinite computations","author":"thomas","year":"1993","journal-title":"A Decade of Concurrency Reflections and Perspectives"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.914952"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2009.5185372"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2013.6580816"},{"journal-title":"Predictive Control for Linear and Hybrid Systems","year":"2015","author":"borrelli","key":"ref66"},{"key":"ref29","first-page":"60","article-title":"Concurrency, compositionality, and correctness","author":"lamport","year":"2010","journal-title":"ch Computer Science and State Machines"},{"key":"ref67","article-title":"Sensing, navigation and reasoning technologies for the DARPA Urban Challenge","author":"burdick","year":"2007","journal-title":"DARPA Urban Challenge Final Report"},{"journal-title":"List of verification and synthesis tools","year":"2013","author":"filippidis","key":"ref68"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2010.5650371"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2007.906923"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/2736348"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/197917.197960"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2016.7525009"},{"key":"ref21","first-page":"911","article-title":"Synthesis of reacive(l) designs","volume":"78","author":"bloem","year":"2012","journal-title":"JCSS"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59042-0_57"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211870"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.01.006"},{"key":"ref25","first-page":"364","article-title":"Synthesis of reactive(l) designs","author":"piterman","year":"2006","journal-title":"VMCAI"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/s11784-012-0071-6"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1979.25"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/123186.123222"},{"journal-title":"A Methodology for Formal Hardware Verification with Application to Microprocessors","year":"1993","author":"beatty","key":"ref58"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1109\/12.73590"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1949.tb03624.x"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"journal-title":"Principles of Model Checking MIT","year":"2008","author":"baier","key":"ref54"},{"key":"ref53","article-title":"Solution of Church's problem: A tutorial","volume":"5","author":"thomas","year":"2008","journal-title":"New Perspectives on Games and Interaction"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2004.1319630"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511546877"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289074"},{"year":"0","key":"ref40","article-title":"po1ytope: Geometric operations on polytopes of any dimension (Python package)"},{"key":"ref12","first-page":"657","article-title":"What good is temporal logic?","volume":"83","author":"lamport","year":"1983","journal-title":"Information Processing"},{"journal-title":"Specifying Systems","year":"2002","author":"lamport","key":"ref13"},{"journal-title":"Formal Methods for Design and Verification of Embedded Control Systems Application to An Autonomous Vehicle","year":"2010","author":"wongpiromsarn","key":"ref14"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6315141"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6225208"},{"key":"ref17","article-title":"Temporal logic: The lesser of three evils","author":"lamport","year":"2010","journal-title":"Amir Pnueli Memorial Symposium NYU"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.23"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"journal-title":"Decision Procedures","year":"2008","author":"kroening","key":"ref4"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-10778-2"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"journal-title":"Studies in hybrid systems modeling analysis and control","year":"1995","author":"branicky","key":"ref7"},{"key":"ref49","article-title":"PEP20: The Zen of Python","author":"peters","year":"2004","journal-title":"Python Enhancement Proposals"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1967701.1967747"},{"year":"0","key":"ref46","article-title":"dd: Decision diagrams (Python package)"},{"year":"0","key":"ref45","article-title":"omega: Symbolic algorithms for solving games of infinite duration (Python package)"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/947955.1083808"},{"year":"0","key":"ref47","article-title":"GNU Linear programming kit, version 4.60"},{"article-title":"Incremental control synthesis for robotics in the presence of temporal logic specifications","year":"2016","author":"livingston","key":"ref42"},{"key":"ref41","first-page":"502","article-title":"Multi-Parametric Toolbox 3.0","author":"herceg","year":"2013","journal-title":"ECC"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.202.6"},{"key":"ref43","article-title":"CUDD: CU Decision Diagram package - v2.5.1","author":"somenzi","year":"2015","journal-title":"Univ of Colorado at Boulder"}],"event":{"name":"2016 IEEE Conference on Control Applications (CCA)","start":{"date-parts":[[2016,9,19]]},"location":"Buenos Aires","end":{"date-parts":[[2016,9,22]]}},"container-title":["2016 IEEE Conference on Control Applications (CCA)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7581720\/7587772\/07587949.pdf?arnumber=7587949","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T18:46:24Z","timestamp":1749667584000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7587949\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":70,"URL":"https:\/\/doi.org\/10.1109\/cca.2016.7587949","relation":{},"subject":[],"published":{"date-parts":[[2016,9]]}}}