{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:24Z","timestamp":1776333504331,"version":"3.51.2"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2012,6,19]],"date-time":"2012-06-19T00:00:00Z","timestamp":1340064000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Auton Robot"],"published-print":{"date-parts":[[2012,10]]},"DOI":"10.1007\/s10514-012-9301-4","type":"journal-article","created":{"date-parts":[[2012,6,18]],"date-time":"2012-06-18T17:52:46Z","timestamp":1340041966000},"page":"309-321","source":"Crossref","is-referenced-by-count":8,"title":["Probabilistic guarantees for high-level robot behavior in the presence of sensor error"],"prefix":"10.1007","volume":"33","author":[{"given":"Benjamin","family":"Johnson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hadas","family":"Kress-Gazit","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,19]]},"reference":[{"key":"9301_CR1","doi-asserted-by":"crossref","first-page":"2689","DOI":"10.1109\/ROBOT.2010.5509503","volume-title":"IEEE international conference on robotics and automation (ICRA)","author":"A. Bhatia","year":"2010","unstructured":"Bhatia, A., Kavraki, L., & Vardi, M. (2010). Sampling-based motion planning with temporal goals. In IEEE international conference on robotics and automation (ICRA) (pp. 2689\u20132696). New York: IEEE Press."},{"key":"9301_CR2","first-page":"572","volume-title":"Proc of IEEE\/RSJ","author":"D. Conner","year":"2007","unstructured":"Conner, D., Kress-Gazit, H., Choset, H., & Rizzi, A. (2007). Valet parking without a valet. In Proc of IEEE\/RSJ (pp. 572\u2013577)."},{"key":"9301_CR3","volume-title":"18th IFAC world congress","author":"X. C. Ding","year":"2011","unstructured":"Ding, X. C., Smith, S. L., Belta, C., & Rus, D. (2011). Ltl control in uncertain environments with probabilistic satisfaction guarantees. In 18th IFAC world congress."},{"key":"9301_CR4","first-page":"995","volume-title":"Handbook of theoretical computer science E","author":"E. Emerson","year":"1990","unstructured":"Emerson, E. (1990). Temporal and modal logic. In Handbook of theoretical computer science E (Vol.\u00a016, pp. 995\u20131072)."},{"key":"9301_CR5","first-page":"4885","volume-title":"Proceedings of the 44th IEEE conference on decision and control","author":"G. Fainekos","year":"2006","unstructured":"Fainekos, G., Kress-Gazit, H., & Pappas, G. (2006). Hybrid controllers for path planning: a\u00a0temporal logic approach. In Proceedings of the 44th IEEE conference on decision and control (pp. 4885\u20134890)."},{"key":"9301_CR6","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/978-3-540-71493-4_18","volume-title":"Hybrid systems: computation and control","author":"G. Fainekos","year":"2007","unstructured":"Fainekos, G., Girard, A., & Pappas, G. (2007). Hierarchical synthesis of hybrid controllers from temporal logic specifications. In Hybrid systems: computation and control (pp. 203\u2013216). Berlin: Springer."},{"key":"9301_CR7","doi-asserted-by":"crossref","first-page":"1988","DOI":"10.1109\/IROS.2010.5650371","volume-title":"IEEE\/RSJ international conference on intelligent robots and systems","author":"C. Finucane","year":"2010","unstructured":"Finucane, C., Jing, G., & Kress-Gazit, H. (2010). LTLMoP: experimenting with language, temporal logic and robot control. In IEEE\/RSJ international conference on intelligent robots and systems, Taipei, Taiwan (pp. 1988\u20131993)."},{"key":"9301_CR8","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E. M. Hahn","year":"2010","unstructured":"Hahn, E. M., Hermanns, H., & Zhang, L. (2010). Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer, 13, 3\u201319.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9301_CR9","volume-title":"Proceedings of robotics: science and systems","author":"B. Johnson","year":"2011","unstructured":"Johnson, B., & Kress-Gazit, H. (2011). Probabilistic analysis of correctness of high-level robot behavior with sensor error. In Proceedings of robotics: science and systems, Los Angeles, CA, USA."},{"key":"9301_CR10","first-page":"330","volume-title":"IEEE international conference on robotics and automation","author":"B. Johnson","year":"2012","unstructured":"Johnson, B., Havlak, F., Campbell, M., & Kress-Gazit, H. (2012). Execution and analysis of high-level tasks with dynamic obstacle anticipation. In IEEE international conference on robotics and automation. (ICRA), Saint Paul, MN (pp. 330\u2013337)"},{"key":"9301_CR11","first-page":"2222","volume-title":"IEEE conference on decision and control","author":"S. Karaman","year":"2009","unstructured":"Karaman, S., & Frazzoli, E. (2009). Sampling-based motion planning with deterministic \u03bc-calculus specifications. In IEEE conference on decision and control (pp. 2222\u20132229)."},{"key":"9301_CR12","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/11730637_26","volume-title":"Hybrid systems: computation and control","author":"M. Kloetzer","year":"2006","unstructured":"Kloetzer, M., & Belta, C. (2006). A fully automated framework for control of linear systems from ltl specifications. In Hybrid systems: computation and control (Vol.\u00a03927, pp. 333\u2013347)."},{"key":"9301_CR13","doi-asserted-by":"crossref","first-page":"3116","DOI":"10.1109\/ROBOT.2007.363946","volume-title":"2007 IEEE international conference on robotics and automation","author":"H. Kress-Gazit","year":"2007","unstructured":"Kress-Gazit, H., Fainekos, G., & Pappas, G. (2007). Where\u2019s Waldo? sensor-based temporal logic motion planning. In 2007 IEEE international conference on robotics and automation (pp. 3116\u20133121)."},{"issue":"6","key":"9301_CR14","doi-asserted-by":"crossref","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H. Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G., & Pappas, G. (2009). Temporal-logic-based reactive mission and motion planning. IEEE Transactions on Robotics, 25(6), 1370\u20131381.","journal-title":"IEEE Transactions on Robotics"},{"key":"9301_CR15","unstructured":"Kwiatkowska, M., Norman, G., & Parker, D. (2001). PRISM: probabilistic symbolic model checker. In P. Kemper (Ed.), Proc. Tools session of Aachen 2001 international multiconference on measurement, modelling and evaluation of computer-communication systems (pp.\u00a07\u201312). Available as technical report 760\/2001, University of Dortmund University of Dortmund."},{"key":"9301_CR16","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal methods for performance evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., & Parker, D. (2007). Stochastic model checking. In Formal methods for performance evaluation (pp. 220\u2013270)."},{"key":"9301_CR17","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., & Kattenbelt, M. (2010). Prism probabilistic model checker. http:\/\/www.prismmodelchecker.org\/ ."},{"key":"9301_CR18","first-page":"2236","volume-title":"IEEE conference on decision and control","author":"M. Lahijanian","year":"2009","unstructured":"Lahijanian, M., Andersson, S., & Belta, C. (2009). A probabilistic approach for control of a stochastic system from ltl specifications. In IEEE conference on decision and control, Shanghai, P.R. China (pp. 2236\u20132241)."},{"key":"9301_CR19","doi-asserted-by":"crossref","first-page":"3227","DOI":"10.1109\/ROBOT.2010.5509686","volume-title":"2010 IEEE international conference on robotics and automation (ICRA)","author":"M. Lahijanian","year":"2010","unstructured":"Lahijanian, M., Wasniewski, J., Andersson, S., & Belta, C. (2010). Motion planning and control from temporal logic specifications with probabilistic satisfaction guarantees. In 2010 IEEE international conference on robotics and automation (ICRA), Anchorage, AK (pp. 3227\u20133232)."},{"key":"9301_CR20","first-page":"153","volume-title":"IEEE conference on decision and control","author":"S. Loizou","year":"2004","unstructured":"Loizou, S., & Kyriakopoulos, K. (2004). Automatic synthesis of multi-agent motion tasks based on ltl specifications. In IEEE conference on decision and control (Vol.\u00a01, pp. 153\u2013158). New York: IEEE Press."},{"key":"9301_CR21","unstructured":"Peterson, P., & Johansson, F. (2011). Sympycore\u2014an efficient pure python computer algebra system. http:\/\/code.google.com\/p\/sympycore\/ ."},{"key":"9301_CR22","first-page":"364","volume-title":"Verification, model checking, and abstract","author":"N. Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., & Sa\u2019ar, Y. (2006). Synthesis of reactive (1) designs. In Verification, model checking, and abstract (pp. 364\u2013380)."},{"issue":"2","key":"9301_CR23","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/j.cosrev.2010.06.002","volume":"5","author":"K. Y. Rozier","year":"2011","unstructured":"Rozier, K. Y. (2011). Linear temporal logic symbolic model checking. Computer Science Review. 5(2), 163\u2013203.","journal-title":"Computer Science Review"},{"key":"9301_CR24","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1007\/3-540-36580-X_36","volume-title":"Hybrid systems: computation and control","author":"P. Tabuada","year":"2003","unstructured":"Tabuada, P., & Pappas, G. (2003). Model checking ltl over controllable linear systems is decidable. In Hybrid systems: computation and control (pp. 498\u2013513)."},{"issue":"12","key":"9301_CR25","doi-asserted-by":"crossref","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","volume":"51","author":"P. Tabuada","year":"2006","unstructured":"Tabuada, P., & Pappas, G. (2006). Linear time logic control of discrete-time linear systems. IEEE Transactions on Automatic Control, 51(12), 1862\u20131877.","journal-title":"IEEE Transactions on Automatic Control"},{"key":"9301_CR26","first-page":"5997","volume-title":"IEEE conference on decision and control (CDC)","author":"T. Wongpiromsarn","year":"2009","unstructured":"Wongpiromsarn, T., Topcu, U., & Murray, R. (2009). Receding horizon temporal logic planning. In IEEE conference on decision and control (CDC), IEEE Press, New York (pp. 5997\u20136004)."},{"key":"9301_CR27","volume-title":"AAAI spring symposium on embedded reasoning: intelligence in embedded systems","author":"T. Wongpiromsarn","year":"2010","unstructured":"Wongpiromsarn, T., Topcu, U., & Murray, R. (2010). Automatic synthesis of robust embedded control software. In AAAI spring symposium on embedded reasoning: intelligence in embedded systems."}],"container-title":["Autonomous Robots"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10514-012-9301-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10514-012-9301-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10514-012-9301-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,30]],"date-time":"2019-06-30T02:54:16Z","timestamp":1561863256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10514-012-9301-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,19]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["9301"],"URL":"https:\/\/doi.org\/10.1007\/s10514-012-9301-4","relation":{},"ISSN":["0929-5593","1573-7527"],"issn-type":[{"value":"0929-5593","type":"print"},{"value":"1573-7527","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,19]]}}}