{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:08:22Z","timestamp":1750219702366,"version":"3.41.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,1,10]],"date-time":"2024-01-10T00:00:00Z","timestamp":1704844800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"MSIT (Ministry of Science and ICT), Korea, under the ITRC","award":["IITP-2023-2020-0-01795"],"award-info":[{"award-number":["IITP-2023-2020-0-01795"]}]},{"name":"(SW Star Lab) Software R&D for Model-based Analysis and Verification of Higher-order Large Complex System","award":["2015-0-00250"],"award-info":[{"award-number":["2015-0-00250"]}]},{"name":"Electronics and Telecommunications Research Institut","award":["23ZS1300"],"award-info":[{"award-number":["23ZS1300"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2024,1,31]]},"abstract":"<jats:p>Cyber-Physical Systems (CPS) continuously interact with their physical environments through embedded software controllers that observe the environments and determine actions. Field Operational Tests (FOT) are essential to verify to what extent the CPS under analysis can achieve certain CPS goals, such as satisfying the safety and performance requirements, while interacting with the real operational environment. However, performing many FOTs to obtain statistically significant verification results is challenging due to its high cost and risk in practice. Simulation-based verification can be an alternative to address the challenge, but it still requires an accurate virtual environment model that can replace the real environment interacting with the CPS in a closed loop.<\/jats:p>\n          <jats:p>In this article, we propose ENVI (ENVironment Imitation), a novel approach to automatically generate an accurate virtual environment model, enabling efficient and accurate simulation-based CPS goal verification in practice.To do this, we first formally define the problem of the virtual environment model generation and solve it by leveraging Imitation Learning (IL), which has been actively studied in machine learning to learn complex behaviors from expert demonstrations. The key idea behind the model generation is to leverage IL for training a model that imitates the interactions between the CPS controller and its real environment as recorded in (possibly very small) FOT logs. We then statistically verify the goal achievement of the CPS by simulating it with the generated model. We empirically evaluate ENVI by applying it to the verification of two popular autonomous driving assistant systems. The results show that ENVI can reduce the cost of CPS goal verification while maintaining its accuracy by generating accurate environment models from only a few FOT logs. The use of IL in virtual environment model generation opens new research directions, further discussed at the end of the article.<\/jats:p>","DOI":"10.1145\/3633804","type":"journal-article","created":{"date-parts":[[2023,11,27]],"date-time":"2023-11-27T14:50:05Z","timestamp":1701096605000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Virtual Environment Model Generation for CPS Goal Verification using Imitation Learning"],"prefix":"10.1145","volume":"23","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6068-5054","authenticated-orcid":false,"given":"Yong-Jun","family":"Shin","sequence":"first","affiliation":[{"name":"ETRI, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0840-6449","authenticated-orcid":false,"given":"Donghwan","family":"Shin","sequence":"additional","affiliation":[{"name":"University of Sheffield, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3152-5219","authenticated-orcid":false,"given":"Doo-Hwan","family":"Bae","sequence":"additional","affiliation":[{"name":"KAIST, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,10]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10618-018-0596-4"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICM48031.2019.9021288"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-803801-7.00019-5"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2897824.2925893"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/AGENTS.2018.8460083"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/CEC.2017.7969377"},{"issue":"1","key":"e_1_3_2_8_2","first-page":"161","article-title":"Cyber-physical systems","volume":"12","author":"Baheti Radhakisan","year":"2011","unstructured":"Radhakisan Baheti and Helen Gill. 2011. Cyber-physical systems. The Impact of Control Technology 12, 1 (2011), 161\u2013166.","journal-title":"The Impact of Control Technology"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","first-page":"2188","DOI":"10.1016\/j.trpro.2016.05.234","article-title":"Methodology for field operational tests of automated vehicles","volume":"14","author":"Barnard Yvonne","year":"2016","unstructured":"Yvonne Barnard, Satu Innamaa, Sami Koskinen, Helena Gellerman, Erik Svanberg, and Haibo Chen. 2016. Methodology for field operational tests of automated vehicles. Transportation Research Procedia 14 (2016), 2188\u20132196.","journal-title":"Transportation Research Procedia"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-73959-1_16"},{"key":"e_1_3_2_11_2","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1007\/978-3-319-74781-1_35","volume-title":"Proceedings of the Software Engineering and Formal Methods","author":"C\u00e1mara Javier","year":"2018","unstructured":"Javier C\u00e1mara, Wenxin Peng, David Garlan, and Bradley Schmerl. 2018. Reasoning About Sensing Uncertainty in Decision-Making for Self-adaptation. In Proceedings of the Software Engineering and Formal Methods, Antonio Cerone and Marco Roveri (Eds.). Springer International Publishing, Cham, 523\u2013540."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2015.2433892"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEAMS.2016.010"},{"key":"e_1_3_2_14_2","first-page":"1117","volume-title":"Proceedings of the International Conference on Artificial Intelligence and Statistics","author":"Guan Ziwei","year":"2021","unstructured":"Ziwei Guan, Tengyu Xu, and Yingbin Liang. 2021. When will generative adversarial imitation learning algorithms attain global convergence. In Proceedings of the International Conference on Artificial Intelligence and Statistics. PMLR, 1117\u20131125."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2019.11.146"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/3157382.3157608"},{"key":"e_1_3_2_17_2","first-page":"20703","article-title":"Model-based imitation learning for urban driving","volume":"35","author":"Hu Anthony","year":"2022","unstructured":"Anthony Hu, Gianluca Corrado, Nicolas Griffiths, Zachary Murez, Corina Gurau, Hudson Yeo, Alex Kendall, Roberto Cipolla, and Jamie Shotton. 2022. Model-based imitation learning for urban driving. Advances in Neural Information Processing Systems 35 (2022), 20703\u201320716.","journal-title":"Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3054912"},{"key":"e_1_3_2_19_2","volume-title":"Intelligent Transport Systems \u2014 Lane Keeping Assistance Systems (LKAS) \u2014 Performance Requirements and Test Procedures","author":"ISO 11270:2014","year":"2014","unstructured":"ISO 11270:2014 2014. Intelligent Transport Systems \u2014 Lane Keeping Assistance Systems (LKAS) \u2014 Performance Requirements and Test Procedures. Standard. International Organization for Standardization."},{"key":"e_1_3_2_20_2","volume-title":"Intelligent Transport Systems \u2014 Adaptive Cruise Control Systems \u2014 Performance Requirements and Test Procedures","author":"ISO 15622:2018","year":"2018","unstructured":"ISO 15622:2018 2018. Intelligent Transport Systems \u2014 Adaptive Cruise Control Systems \u2014 Performance Requirements and Test Procedures. Standard. International Organization for Standardization."},{"issue":"1","key":"e_1_3_2_21_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3419742","article-title":"Verifying the safety of autonomous systems with neural network controllers","volume":"20","author":"Ivanov Radoslav","year":"2020","unstructured":"Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George J. Pappas, and Insup Lee. 2020. Verifying the safety of autonomous systems with neural network controllers. ACM Transactions on Embedded Computing Systems 20, 1 (2020), 1\u201326.","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"e_1_3_2_22_2","unstructured":"Rohit Jena Changliu Liu and Katia Sycara. 2021. Augmenting GAIL with BC for sample efficient imitation learning. In Proceedings of the 2020 Conference on Robot Learning (Proceedings of Machine Learning Research Vol. 155) Jens Kober FabioRamos and ClaireTomlin (Eds.). PMLR 80\u201390. https:\/\/proceedings.mlr.press\/v155\/jena21a.html"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2022.3192720"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04898-2_327"},{"key":"e_1_3_2_25_2","unstructured":"Diederik P. Kingma and Jimmy Ba. 2015. Adam: A method for stochastic optimization. In 3rd International Conference on Learning Representations (ICLR\u201915) Yoshua Bengio and Yann LeCun (Eds.). San Diego CA."},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Proceedings of the International Conference on Runtime Verification","author":"Legay Axel","year":"2010","unstructured":"Axel Legay, Beno\u00eet Delahaye, and Saddek Bensalem. 2010. Statistical model checking: An overview. In Proceedings of the International Conference on Runtime Verification. Springer, 122\u2013135."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61264-5_5"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3149180"},{"key":"e_1_3_2_29_2","first-page":"702","volume-title":"Proceedings of the 2017 IEEE 14th International Conference on Networking, Sensing and Control","author":"Nguyen Thuy","year":"2017","unstructured":"Thuy Nguyen. 2017. A modelling & simulation based engineering approach for socio-cyber-physical systems. In Proceedings of the 2017 IEEE 14th International Conference on Networking, Sensing and Control. IEEE, 702\u2013707."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.proeng.2012.09.545"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3394486.3403186"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.3390\/info11120588"},{"key":"e_1_3_2_33_2","first-page":"8026","volume-title":"PyTorch: An Imperative Style, High-Performance Deep Learning Library","author":"Paszke Adam","year":"2019","unstructured":"Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas K\u00f6pf, Edward Yang, Zach DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. 2019. PyTorch: An Imperative Style, High-Performance Deep Learning Library. Curran Associates Inc., Red Hook, NY, 8026\u20138037."},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/1953048.2078195"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3197517.3201311"},{"issue":"3","key":"e_1_3_2_36_2","first-page":"686","article-title":"A combined simulation and test case generation strategy for self-adaptive systems","volume":"7","author":"P\u00fcschel Georg","year":"2014","unstructured":"Georg P\u00fcschel, Christian Piechnick, Sebastian G\u00f6tz, Christoph Seidl, Sebastian Richly, Thomas Schlegel, and Uwe A\u00dfmann. 2014. A combined simulation and test case generation strategy for self-adaptive systems. Journal On Advances in Software 7, 3&4 (2014), 686\u2013696.","journal-title":"Journal On Advances in Software"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2016.07.002"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0045-7949(01)00039-6"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/SASO.2018.00019"},{"key":"e_1_3_2_40_2","first-page":"1040","volume-title":"Proceedings of the Advances in Neural Information Processing Systems","author":"Schaal Stefan","year":"1996","unstructured":"Stefan Schaal. 1996. Learning from Demonstration. In Proceedings of the Advances in Neural Information Processing Systems. 1040\u20131046. Retrieved from http:\/\/papers.nips.cc\/paper\/1224-learning-from-demonstration"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.neunet.2021.03.035"},{"key":"e_1_3_2_42_2","unstructured":"John Schulman Filip Wolski Prafulla Dhariwal Alec Radford and Oleg Klimov. 2017. Proximal Policy Optimization Algorithms. arxiv:1707.06347 Retrieved from https:\/\/arxiv.org\/abs\/1707.06347"},{"key":"e_1_3_2_43_2","unstructured":"Mark R. Segal. 2004. Machine learning benchmarks and random forest regression. Technical Report. UCSF: Center for Bioinformatics and Molecular Biostatistics."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1109\/APSEC53868.2021.00037"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/978-3-030-71500-7_15","volume-title":"Proceedings of the International Conference on Fundamental Approaches to Software Engineering","author":"Shin Yong-Jun","year":"2021","unstructured":"Yong-Jun Shin, Eunho Cho, and Doo-Hwan Bae. 2021. Pasta: An efficient proactive adaptation approach based on statistical model checking for self-adaptive systems. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering. Springer International Publishing Cham, 292\u2013312."},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/SEAMS51251.2021.00038"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA40945.2020.9197020"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3362098"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/TNN.1998.712192"},{"key":"e_1_3_2_50_2","article-title":"Policy gradient methods for reinforcement learning with function approximation","volume":"12","author":"Sutton Richard S.","year":"1999","unstructured":"Richard S. Sutton, David McAllester, Satinder Singh, and Yishay Mansour. 1999. Policy gradient methods for reinforcement learning with function approximation. In Proceedings of the Advances in Neural Information Processing Systems 12 (1999).","journal-title":"In Proceedings of the Advances in Neural Information Processing Systems"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606552"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3358230"},{"key":"e_1_3_2_53_2","doi-asserted-by":"crossref","first-page":"274","DOI":"10.1109\/Humanoids43949.2019.9034991","volume-title":"Proceedings of the 2019 IEEE-RAS 19th International Conference on Humanoid Robots (Humanoids)","author":"Tsurumine Yoshihisa","year":"2019","unstructured":"Yoshihisa Tsurumine, Yunduan Cui, Kimitoshi Yamazaki, and Takamitsu Matsubara. 2019. Generative adversarial imitation learning with deep p-network for robotic cloth manipulation. In Proceedings of the 2019 IEEE-RAS 19th International Conference on Humanoid Robots (Humanoids). IEEE, 274\u2013280."},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3483380"},{"issue":"5","key":"e_1_3_2_55_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3358232","article-title":"Statistical verification of hyperproperties for cyber-physical systems","volume":"18","author":"Wang Yu","year":"2019","unstructured":"Yu Wang, Mojtaba Zarei, Borzoo Bonakdarpour, and Miroslav Pajic. 2019. Statistical verification of hyperproperties for cyber-physical systems. ACM Transactions on Embedded Computing Systems 18, 5s (2019), 1\u201323.","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1080\/17517575.2018.1442934"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2017.12.009"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/LWC.2021.3051688"},{"issue":"4","key":"e_1_3_2_59_2","doi-asserted-by":"crossref","first-page":"3871","DOI":"10.1109\/TASE.2021.3138280","article-title":"Explainable hierarchical imitation learning for robotic drink pouring","volume":"19","author":"Zhang Dandan","year":"2021","unstructured":"Dandan Zhang, Qiang Li, Yu Zheng, Lei Wei, Dongsheng Zhang, and Zhengyou Zhang. 2021. Explainable hierarchical imitation learning for robotic drink pouring. IEEE Transactions on Automation Science and Engineering 19, 4 (2021), 3871\u20133887.","journal-title":"IEEE Transactions on Automation Science and Engineering"},{"key":"e_1_3_2_60_2","first-page":"12805","volume-title":"Proceedings of the Advances in Neural Information Processing Systems","volume":"33","author":"Zhang Xin","year":"2020","unstructured":"Xin Zhang, Yanhua Li, Ziming Zhang, and Zhi-Li Zhang. 2020. f-GAIL: Learning f-Divergence for Generative Adversarial Imitation Learning. In Proceedings of the Advances in Neural Information Processing Systems, H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin (Eds.), Vol. 33. Curran Associates, Inc., 12805\u201312815. Retrieved from https:\/\/proceedings.neurips.cc\/paper\/2020\/file\/967990de5b3eac7b87d49a13c6834978-Paper.pdf"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1109\/TBDATA.2020.3039810"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633804","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3633804","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:35:48Z","timestamp":1750178148000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3633804"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,10]]},"references-count":60,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1,31]]}},"alternative-id":["10.1145\/3633804"],"URL":"https:\/\/doi.org\/10.1145\/3633804","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2024,1,10]]},"assertion":[{"value":"2022-08-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-06","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}