{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T04:32:48Z","timestamp":1782966768373,"version":"3.54.5"},"reference-count":26,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"1","license":[{"start":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T00:00:00Z","timestamp":1359676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Robot."],"published-print":{"date-parts":[[2013,2]]},"DOI":"10.1109\/tro.2012.2214558","type":"journal-article","created":{"date-parts":[[2012,9,12]],"date-time":"2012-09-12T21:18:08Z","timestamp":1347484688000},"page":"94-104","source":"Crossref","is-referenced-by-count":40,"title":["Explaining Impossible High-Level Robot Behaviors"],"prefix":"10.1109","volume":"29","author":[{"given":"Vasumathi","family":"Raman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hadas","family":"Kress-Gazit","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2010.5650371"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"663","DOI":"10.1007\/978-3-642-22110-1_54","article-title":"Analyzing unsynthesizable specifications for high-level robot behavior using LTLMoP","author":"raman","year":"2011","journal-title":"Comput Aided Verif"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6224807"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1163\/156855308X344864"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"ref17","first-page":"171","article-title":"JTLV: A framework for developing verification algorithms","author":"pnueli","year":"2010","journal-title":"Proc 22nd Int Conf Comput Aided Verif"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1959.tb01585.x"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2011.5979895"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2011.942115"},{"key":"ref3","first-page":"2222","article-title":"Sampling-based motion planning with deterministic <formula formulatype=\"inline\"><tex Notation=\"TeX\">$\\mu$<\/tex> <\/formula>-calculus specifications","author":"karaman","year":"2009","journal-title":"Proc IEEE Conf Decis Control"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref5","year":"0"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"ref7","author":"piterman","year":"2006","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.914952"},{"key":"ref9","first-page":"101","article-title":"Receding horizon control for temporal logic specifications","author":"wongpiromsarn","year":"2010","journal-title":"Proc ACM Int Conf Hybrid Syst Comput Control"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73370-6_11"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_53"},{"key":"ref21","first-page":"129","article-title":"Towards a notion of unsatisfiable cores for LTL","author":"schuppan","year":"2009","journal-title":"Proc Fundam Softw Eng"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78163-9_9"},{"key":"ref23","first-page":"94","article-title":"Explaining counterexamples using causality","author":"beer","year":"2009","journal-title":"Comput Aided Verif"},{"key":"ref26","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14295-6_37","article-title":"RATSY - a new requirements analysis tool with synthesis","author":"bloem","year":"2010","journal-title":"Comput Aided Verif"},{"key":"ref25","first-page":"147","article-title":"Environment assumptions for synthesis","author":"chatterjee","year":"2008","journal-title":"Proc 19th Int Conf Concurrency Thoery"}],"container-title":["IEEE Transactions on Robotics"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8860\/6428720\/06301745.pdf?arnumber=6301745","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:38:08Z","timestamp":1642005488000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6301745\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,2]]},"references-count":26,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.1109\/tro.2012.2214558","relation":{},"ISSN":["1552-3098","1941-0468"],"issn-type":[{"value":"1552-3098","type":"print"},{"value":"1941-0468","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,2]]}}}