{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:58:10Z","timestamp":1769727490869,"version":"3.49.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T00:00:00Z","timestamp":1649635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JST ERATO","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}]},{"name":"JST CREST","award":["JPMJCR2012"],"award-info":[{"award-number":["JPMJCR2012"]}]},{"name":"JSPS Grant-in-Aid for Young Scientists","award":["JP21K14184"],"award-info":[{"award-number":["JP21K14184"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2022,4,30]]},"abstract":"<jats:p>This article investigates a collaborative rover-copter path planning and exploration with temporal logic specifications under uncertain environments. The objective of the rover is to complete a mission expressed by a syntactically co-safe linear temporal logic (scLTL) formula, while the objective of the copter is to actively explore the environment and reduce its uncertainties, aiming at assisting the rover and enhancing the efficiency of the mission completion. To formalize our approach, we first capture the environmental uncertainties by environmental beliefs of the atomic propositions, under an assumption that it is unknown which properties (or, atomic propositions) are satisfied in each area of the environment. The environmental beliefs of the atomic propositions are updated according to the Bayes rule based on the Bernoulli-type sensor measurements provided by both the rover and the copter. Then, the optimal policy for the rover is synthesized by maximizing a belief of the satisfaction of the scLTL formula through an implementation of an automata-based model checking. An exploration policy for the copter is then synthesized by employing the notion of an entropy that is evaluated based on the environmental beliefs of the atomic propositions, and a path that the rover intends to follow according to the optimal policy. As such, the copter can actively explore regions whose uncertainties are high and that are relevant to the mission completion. Finally, some numerical examples illustrate the effectiveness of the proposed approach.<\/jats:p>","DOI":"10.1145\/3470453","type":"journal-article","created":{"date-parts":[[2022,2,4]],"date-time":"2022-02-04T21:44:21Z","timestamp":1644011061000},"page":"1-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Collaborative Rover-copter Path Planning and Exploration with Temporal Logic Specifications Based on Bayesian Update Under Uncertain Environments"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9376-5760","authenticated-orcid":false,"given":"Kazumune","family":"Hashimoto","sequence":"first","affiliation":[{"name":"Graduate School of Engineering, Osaka University, Toyonaka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natsuko","family":"Tsumagari","sequence":"additional","affiliation":[{"name":"Graduate School of Engineering and Science, Osaka University, Toyonaka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toshimitsu","family":"Ushio","sequence":"additional","affiliation":[{"name":"Graduate School of Engineering and Science, Osaka University, Toyonaka, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,4,11]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-5574-4"},{"key":"e_1_3_3_3_2","first-page":"1","volume-title":"Proceedings of the AIAA Atmospheric Flight Mechanics Conference","year":"2018","unstructured":"B. Balaram, T. Canham, C. Duncan, H. F. Grip, W. Johnson, J. Maki, A. Quon, R. Stern, and D. Zhu. 2018. Mars helicopter technology demonstrator. In Proceedings of the AIAA Atmospheric Flight Mechanics Conference. 1\u201318."},{"key":"e_1_3_3_4_2","volume-title":"Proceedings of the NASA\/JPL News Release","year":"2018","unstructured":"B. Dwayne and W. JoAnna. 2018. Mars helicopter to fly on NASA\u2019s next red planet rover mission. In Proceedings of the NASA\/JPL News Release."},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2018.XIV.047"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2018.8619683"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/LRA.2020.2970650"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1146\/annurev-control-060117-104838"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2007.339624"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-50763-7"},{"key":"e_1_3_3_11_2","volume-title":"Principles of Model Checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P Katoen. 2008. Principles of Model Checking. The MIT Press."},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2005.1583068"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/1702315.1702639"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2007.899155"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/SMC.2013.340"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2013.6697120"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2016.7487554"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461380"},{"key":"e_1_3_3_19_2","volume-title":"Proceedings of the IEEE International Conference on Robotics and Automation.","author":"Guo M.","year":"2013","unstructured":"M. Guo, K. H. Johansson, and D. V. Dimarogonas. 2013. Revising motion planning under linear temporal logic specifications in partially known workspaces. In Proceedings of the IEEE International Conference on Robotics and Automation."},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364914546174"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2018.2799561"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6225208"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426524"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509686"},{"key":"e_1_3_3_25_2","unstructured":"C. Yoo and C. Belta. 2015. Control with probabilistic signal temporal logic. arXiv:1510.08474. Retrieved from https:\/\/arxiv.org\/abs\/1510.08474."},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7799415"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364919846340"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426174"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364913519000"},{"key":"e_1_3_3_31_2","unstructured":"K. Hashimoto A. Saoud M. Kishida T. Ushio and D. V. Dimarogonas. 2020. Learning-based symbolic abstractions for nonlinear control systems. . arXiv:2004.01879. Retrieved from https:\/\/arxiv.org\/abs\/2004.01879"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039527"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364915581505"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2018.8431181"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC40024.2019.9028919"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2013.6696434"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1177\/0278364914562980"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3243216"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2020.01.009"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_5"},{"key":"e_1_3_3_41_2","volume-title":"Elements of Information Theory","author":"Cover T. M.","year":"2006","unstructured":"T. M. Cover and J. A. Thomas. 2006. Elements of Information Theory. Wiley Series."},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.03.027"},{"key":"e_1_3_3_43_2","unstructured":"Retrieved on 14 March 2021 from https:\/\/drive.google.com\/file\/d\/1tFbnI2ZAeK5rXyYeyCK4cpi0OY6QsOA-\/view."}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3470453","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3470453","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:26Z","timestamp":1750188626000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3470453"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,11]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4,30]]}},"alternative-id":["10.1145\/3470453"],"URL":"https:\/\/doi.org\/10.1145\/3470453","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"value":"2378-962X","type":"print"},{"value":"2378-9638","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,11]]},"assertion":[{"value":"2020-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-06-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-04-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}