{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T21:10:39Z","timestamp":1651785039649},"reference-count":43,"publisher":"IGI Global","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"abstract":"<jats:p>One approach to determining whether an automated system is performing correctly is to monitor its performance, signaling when the performance is not acceptable; another approach is to automatically analyze the possible behaviors of the system a-priori and determine performance guarantees. Thea authors have applied this second approach to automatically derive performance guarantees for behavior-based, multi-robot critical mission software using an innovative approach to formal verification for robotic software. Localization and mapping algorithms can allow a robot to navigate well in an unknown environment. However, whether such algorithms enhance any specific robot mission is currently a matter for empirical validation. Several approaches to incorporating pre-existing software into the authors' probabilistic verification framework are presented, and one used to include Monte-Carlo based localization software. Verification and experimental validation results are discussed for real localization missions with this software, showing that the proposed approach accurately predicts performance.<\/jats:p>","DOI":"10.4018\/ijmstr.2017010103","type":"journal-article","created":{"date-parts":[[2017,5,31]],"date-time":"2017-05-31T17:50:08Z","timestamp":1496253008000},"page":"49-70","source":"Crossref","is-referenced-by-count":1,"title":["Establishing A-Priori Performance Guarantees for Robot Missions that Include Localization Software"],"prefix":"10.4018","volume":"5","author":[{"given":"Damian","family":"Lyons","sequence":"first","affiliation":[{"name":"Department of Computer and Information Science, Fordham University, New York City, NY, USA"}]},{"given":"Ronald C","family":"Arkin","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, Atlanta, GA, USA"}]},{"given":"Shu","family":"Jiang","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, Atlanta, GA, USA"}]},{"given":"Matthew J","family":"O'Brien","sequence":"additional","affiliation":[{"name":"Georgia Institute of Technology, Atlanta, GA, USA"}]},{"given":"Feng","family":"Tang","sequence":"additional","affiliation":[{"name":"Fordham University, New York City, NY, USA"}]},{"given":"Peng","family":"Tang","sequence":"additional","affiliation":[{"name":"Fordham University, New York City, NY, USA"}]}],"member":"2432","reference":[{"key":"IJMSTR.2017010103-0","author":"R. C.Arkin","year":"1998","journal-title":"Behavior-Based Robots"},{"key":"IJMSTR.2017010103-1","author":"C.Baeir","year":"2008","journal-title":"Introduction to Model Checking"},{"key":"IJMSTR.2017010103-2","doi-asserted-by":"crossref","unstructured":"Bailey, T., & Durrant-Whyte, H. (June, September 2006). Simultaneous Localization and Mapping (DLAM): Party I, II. IEEE Robotics and Automation Magazine.","DOI":"10.1109\/MRA.2006.1678144"},{"key":"IJMSTR.2017010103-3","doi-asserted-by":"crossref","unstructured":"Blackman, S. (2004). Multiple Hypothesis Tracking for Multiple Target Tracking. IEEE A&E Systems Magazine, 19(1).","DOI":"10.1109\/MAES.2004.1263228"},{"key":"IJMSTR.2017010103-4","unstructured":"Brahman, J. (2009). Verification and Analysis of Goal-Based Hybrid Control Systems [Thesis]. P.D. California Institute of Technology, Pasadena, CA."},{"key":"IJMSTR.2017010103-5","doi-asserted-by":"crossref","unstructured":"Cowley, A., & Taylor, C. (2011). Towards Language-Based Verification of Robot Behaviors. Proceedings of the 2011 IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS).","DOI":"10.1109\/IROS.2011.6095028"},{"key":"IJMSTR.2017010103-6","doi-asserted-by":"crossref","unstructured":"Dellaert, F., Fox, D., Burgard, W., & Thrun, S. (1999). Monte Carlo localization for mobile robots. Proceedings of theIEEE Int. Conf. on Rob. & Aut., Detroit.","DOI":"10.1109\/ROBOT.1999.772544"},{"issue":"9","key":"IJMSTR.2017010103-7","first-page":"54","article-title":"Satisfiability Modulo Theories: Introduction and applications.","volume":"54","author":"L.DeMoura","year":"2012","journal-title":"Communications of the ACM"},{"key":"IJMSTR.2017010103-8","doi-asserted-by":"publisher","DOI":"10.1145\/2500468.2494558"},{"key":"IJMSTR.2017010103-9","author":"D.Fox","year":"2001","journal-title":"KLD\u2013Sampling: Adaptive Particle Filters. Neural Information Processing Systems 14"},{"key":"IJMSTR.2017010103-10","doi-asserted-by":"crossref","unstructured":"Huang, J., Erdogan, C., Zhang, Y., Moore, B., Luo, Q., Sundaresan, A., & Rosu, G. (2014). ROSRV: Runtime Verification for Robots. Proceedings of the14th International Conference on Runtime Verification, Toronto.","DOI":"10.1007\/978-3-319-11164-3_20"},{"key":"IJMSTR.2017010103-11","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"IJMSTR.2017010103-12","doi-asserted-by":"crossref","unstructured":"Jiang, S., & Arkin, R. (2015). SLAM-Based Spatial Memory for Behavior-Based Robots. Proceedings of the11th IFAC Symposium on Robot Control (SYROCO), Salvador, Brazil.","DOI":"10.1016\/j.ifacol.2015.12.033"},{"key":"IJMSTR.2017010103-13","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P. (2010). Advances in Probabilistic Model Checking. Proceedings of the11th International Conference VMCAI \u201810, Madrid Spain.","DOI":"10.1007\/978-3-642-11319-2_5"},{"key":"IJMSTR.2017010103-14","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2015.08.002"},{"key":"IJMSTR.2017010103-15","unstructured":"Kim, M., Kang, K.-C., & Lee, H. (2005). Formal Verification of Robot Movements - a Case Study on Home Service Robot SHR100. Proceedings of theIEEE Int. Conf. Robotics and Automation."},{"key":"IJMSTR.2017010103-16","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2004.1308780"},{"key":"IJMSTR.2017010103-17","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Wongpiromsarn, T., & Topcu, U. (2011). Correct, Reactive Robot Control from Abstraction and Temporal Logic Specifications. IEEE Rob. & Aut. Mag., 18(3).","DOI":"10.1109\/MRA.2011.942116"},{"key":"IJMSTR.2017010103-18","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0140-2"},{"key":"IJMSTR.2017010103-19","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.08.004"},{"key":"IJMSTR.2017010103-20","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6225208"},{"key":"IJMSTR.2017010103-21","doi-asserted-by":"crossref","unstructured":"Lyons, D., Arkin, R., Jiang, S., Harrington, D., & Liu, T. (2014). Verifying and Validating Multirobot Missions. Proceedings of theIEEE\/RSJ Int. Conf. on Robots and Systems, Chicago.","DOI":"10.1109\/IROS.2014.6942754"},{"key":"IJMSTR.2017010103-22","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2015.22"},{"key":"IJMSTR.2017010103-23","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2016.0025"},{"key":"IJMSTR.2017010103-24","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2015.2418592"},{"key":"IJMSTR.2017010103-25","doi-asserted-by":"publisher","DOI":"10.3182\/20130626-3-AU-2035.00034"},{"key":"IJMSTR.2017010103-26","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2013.6697122"},{"key":"IJMSTR.2017010103-27","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008807102993"},{"key":"IJMSTR.2017010103-28","doi-asserted-by":"crossref","unstructured":"O'Brien, M., & Arkin, R. (2016). An Analysis of Displays for Probabilistic Robotic Mission Verification Results. Proceedings of the7th International Conference on Applied Human Factors and Ergonomics, Las Vegas NV.","DOI":"10.1007\/978-3-319-41959-6_33"},{"key":"IJMSTR.2017010103-29","doi-asserted-by":"crossref","unstructured":"O'Brien, M., Arkin, R., Harrington, D., Lyons, D., & Jiang, S. (2014). Automatic Verification of Autonomous Robot Missions. Proceedings of the4th Int. Conf. on Simulation, Modelling and Prog. for Aut. Robots, Bergamo, Italy.","DOI":"10.1007\/978-3-319-11900-7_39"},{"key":"IJMSTR.2017010103-30","unstructured":"Piterman, N., Pneuli, A., & Sa'ar, Y. (2006). Synthesis of Reactive(1) Designs. Proceedings of the7th International Conference VMCAI \u201806, Charlestown SC."},{"key":"IJMSTR.2017010103-31","unstructured":"Proetzsch, M., Berns, K., Schuele, T., & Schneider, K. (2007). Formal Verification Of Safety Behaviours Of The Outdoor Robot Ravon. Proceedings of the4th Int. Conf. on Informatics, Automation and Control, Dortmund, Germany."},{"key":"IJMSTR.2017010103-32","unstructured":"Ropertz, T., & Berns, R. (2014). Verification of behavior-based networks-using satisfiability modulo theories. Proceedings of the41st International Symposium on RoboticsISR\/Robotik \u201814."},{"key":"IJMSTR.2017010103-33","author":"S.Russel","year":"2010","journal-title":"Artificial Intelligence"},{"key":"IJMSTR.2017010103-34","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592437"},{"key":"IJMSTR.2017010103-35","author":"S.Thrun","year":"2005","journal-title":"Probabilistic Robotics"},{"key":"IJMSTR.2017010103-36","doi-asserted-by":"crossref","unstructured":"Trojanek, P., & Eder, K. (2014). Verification and testing of mobile robot navigation algorithms. Proceedings of theIEEE\/RSJ Int. Conf on Intelligent Robots and Systems (IROS), Chicago.","DOI":"10.1109\/IROS.2014.6942753"},{"issue":"1","key":"IJMSTR.2017010103-37","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/1387830.1387836","article-title":"A practical approach to formal software verification by static analysis.","volume":"27","author":"A.Venet","year":"2008","journal-title":"ACM SIGAda Letters"},{"key":"IJMSTR.2017010103-38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15651-9_26"},{"key":"IJMSTR.2017010103-39","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2003.1272482"},{"key":"IJMSTR.2017010103-40","unstructured":"Wongpiromsarn, T., & Murray, R. (2008). Formal Verification of an Autonomous Vehicle System. Proceedings of theConference on Decision and Control."},{"key":"IJMSTR.2017010103-41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_17"},{"key":"IJMSTR.2017010103-42","doi-asserted-by":"crossref","unstructured":"Zaks, A., & Joshi, R. (2008). Verifying Multi-threaded C programs with SPIN. Proceedings of the15th International SPIN Workshop, Los Angeles CA.","DOI":"10.1007\/978-3-540-85114-1_22"}],"container-title":["International Journal of Monitoring and Surveillance Technologies Research"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=182506","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,5]],"date-time":"2022-05-05T20:31:37Z","timestamp":1651782697000},"score":1,"resource":{"primary":{"URL":"http:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/IJMSTR.2017010103"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":43,"journal-issue":{"issue":"1"},"URL":"https:\/\/doi.org\/10.4018\/ijmstr.2017010103","relation":{},"ISSN":["2166-7241","2166-725X"],"issn-type":[{"value":"2166-7241","type":"print"},{"value":"2166-725X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,1]]}}}