{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T07:42:16Z","timestamp":1758267736098,"version":"3.28.0"},"reference-count":23,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1109\/cdc.2017.8263808","type":"proceedings-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T15:30:57Z","timestamp":1516721457000},"page":"1132-1137","source":"Crossref","is-referenced-by-count":37,"title":["Linear temporal logic motion planning for teams of underactuated robots using satisfiability modulo convex programming"],"prefix":"10.1109","author":[{"given":"Yasser","family":"Shoukry","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierluigi","family":"Nuzzo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ayca","family":"Balkan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Indranil","family":"Saha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George J.","family":"Pappas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paulo","family":"Tabuada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2014.6907641"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400278"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509503"},{"key":"ref13","first-page":"3743","article-title":"An efficient retraction-based RRT planner","author":"zhang","year":"0","journal-title":"IEEE Int Conf Robotics and Automation"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7799298"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049819"},{"key":"ref16","first-page":"71","article-title":"CaICS: SMT solving for non-linear convex constraints","author":"nuzzo","year":"0","journal-title":"Int Conf Formal Methods in Computer-Aided Design"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"ref19","first-page":"337","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Proc Int Conf Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2012.2195811"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.08.008"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942758"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2013.2295764"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.3233\/AIC-150682"},{"key":"ref7","first-page":"4817","article-title":"Sampling-based temporal logic path planning","author":"vasile","year":"0","journal-title":"Intelligent Robots and Systems (IROS) 2013 IEEE\/RSJ International Conference on"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2006.886494"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1002\/rnc.1715"},{"journal-title":"IBM ILOG CPLEX Optimizer","year":"2012","key":"ref20"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2010.2047820"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.3.2.157"},{"key":"ref23","first-page":"208","article-title":"dReal: An SMT solver for nonlinear theories over the reals","volume":"7898","author":"gao","year":"0","journal-title":"Proceedings of the International Conference on Automated Deduction"}],"event":{"name":"2017 IEEE 56th Annual Conference on Decision and Control (CDC)","start":{"date-parts":[[2017,12,12]]},"location":"Melbourne, Australia","end":{"date-parts":[[2017,12,15]]}},"container-title":["2017 IEEE 56th Annual Conference on Decision and Control (CDC)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8253407\/8263624\/08263808.pdf?arnumber=8263808","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,2,28]],"date-time":"2018-02-28T15:48:12Z","timestamp":1519832892000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/8263808\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/cdc.2017.8263808","relation":{},"subject":[],"published":{"date-parts":[[2017,12]]}}}