{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T04:15:18Z","timestamp":1743567318502,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031851339"},{"type":"electronic","value":"9783031851346"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-85134-6_1","type":"book-chapter","created":{"date-parts":[[2025,3,20]],"date-time":"2025-03-20T04:01:07Z","timestamp":1742443267000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Modelling Cyber-Physical Systems for\u00a0Verification and\u00a0Synthesis"],"prefix":"10.1007","author":[{"given":"Rong","family":"Gu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,3,21]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"1_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bakirtzis, G., Vasilakopoulou, C., Fleming, C.H.: Compositional cyber-physical systems modeling. arXiv preprint arXiv:2101.10484 (2021)","DOI":"10.4204\/EPTCS.333.9"},{"key":"1_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2021.111081","volume":"183","author":"A Bari\u0161i\u0107","year":"2022","unstructured":"Bari\u0161i\u0107, A., et al.: Multi-paradigm modeling for cyber-physical systems: a systematic mapping review. J. Syst. Softw. 183, 111081 (2022)","journal-title":"J. Syst. Softw."},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H., et al.: Formal methods in industry. Form. Asp. Comput. (2024). https:\/\/doi.org\/10.1145\/3689374","DOI":"10.1145\/3689374"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"1613","DOI":"10.1007\/s10270-017-0642-5","volume":"18","author":"S Bliudze","year":"2019","unstructured":"Bliudze, S., Furic, S., Sifakis, J., Viel, A.: Rigorous design of cyber-physical systems: linking physicality and computation. Softw. Syst. Model. 18, 1613\u20131636 (2019)","journal-title":"Softw. Syst. Model."},{"issue":"3","key":"1_CR7","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u00e1r, Y.: Synthesis of reactive (1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Broman, D., Lee, E.A., Tripakis, S., T\u00f6rngren, M.: Viewpoints, formalisms, languages, and tools for cyber-physical systems. In: Proceedings of the 6th International Workshop on Multi-Paradigm Modeling, pp. 49\u201354 (2012)","DOI":"10.1145\/2508443.2508452"},{"key":"1_CR9","unstructured":"Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. J. Symb. Logic 28(4) (1963)"},{"key":"1_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2022.103782","volume":"313","author":"M Cleaveland","year":"2022","unstructured":"Cleaveland, M., Lindemann, L., Ivanov, R., Pappas, G.J.: Risk verification of stochastic systems with neural network controllers. Artif. Intell. 313, 103782 (2022)","journal-title":"Artif. Intell."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Fan, C., Miller, K., Mitra, S.: Fast and guaranteed safe controller synthesis for nonlinear vehicle models. In: International Conference on Computer Aided Verification, pp. 629\u2013652. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-53288-8_31"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Gu, R.: Model checking for reinforcement learning in autonomous driving: one can do more than you think! In: Luckcuck, M., Xu, M. (eds.) Proceedings Sixth International Workshop on Formal Methods for Autonomous Systems, Manchester, UK, 11th and 12th of November 2024. Electronic Proceedings in Theoretical Computer Science, vol.\u00a0411, pp. 160\u2013177. Open Publishing Association (2024). https:\/\/doi.org\/10.4204\/EPTCS.411.11","DOI":"10.4204\/EPTCS.411.11"},{"key":"1_CR13","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102894","volume":"224","author":"R Gu","year":"2022","unstructured":"Gu, R., Jensen, P.G., Seceleanu, C., Enoiu, E., Lundqvist, K.: Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems. Sci. Comput. Program. 224, 102894 (2022)","journal-title":"Sci. Comput. Program."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Gu, R., Moezkarimi, Z., Sirjani, M.: Guess and then check: controller synthesis for safe and secure cyber-physical systems. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems, pp. 230\u2013238. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-62645-6_13"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Gu, R., Seceleanu, C., Enoiu, E., Lundqvist, K.: Model checking collision avoidance of nonlinear autonomous vehicles. In: Formal Methods: 24th International Symposium, FM 2021, pp. 676\u2013694. Springer, Cham (2021)","DOI":"10.1007\/978-3-030-90870-6_37"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Gu, R., Tan, K., H\u00f8eg-Petersen, A.H., Feng, L., Larsen, K.G.: Commonupproad: a framework of formal modelling, verifying, learning, and visualisation of autonomous vehicles (2024). https:\/\/arxiv.org\/abs\/2408.01093","DOI":"10.1007\/978-3-031-75380-0_22"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Hartmanns, A.: Correct probabilistic model checking with floating-point arithmetic. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 41\u201359. Springer, Cham (2022)","DOI":"10.1007\/978-3-030-99527-0_3"},{"issue":"1","key":"1_CR18","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Ivan\u010di\u0107, F., Ganai, M.K., Sankaranarayanan, S., Gupta, A.: Numerical stability analysis of floating-point computations using software model checking. In: Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010), pp. 49\u201358. IEEE (2010)","DOI":"10.1109\/MEMCOD.2010.5558622"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Jaghoori, M.M., Movaghar, A., Sirjani, M.: Modere: the model-checking engine of Rebeca. In: Proceedings of the 2006 ACM Symposium on Applied Computing, pp. 1810\u20131815 (2006)","DOI":"10.1145\/1141277.1141704"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer, B., Lorber, F., Jansen, N., Bloem, R.: Shield synthesis for reinforcement learning. In: Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, 20\u201330 October 2020, Proceedings, Part I 9, pp. 290\u2013306. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-61362-4_16"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u1ef3, J., Meggendorfer, T., Prokop, M., Rieder, S.: Guessing winning policies in LTL synthesis by semantic learning. In: International Conference on Computer Aided Verification, pp. 390\u2013414. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37706-8_20"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"3","key":"1_CR24","doi-asserted-by":"publisher","first-page":"4837","DOI":"10.3390\/s150304837","volume":"15","author":"EA Lee","year":"2015","unstructured":"Lee, E.A.: The past, present and future of cyber-physical systems: a focus on models. Sensors 15(3), 4837\u20134869 (2015)","journal-title":"Sensors"},{"issue":"1","key":"1_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2912149","volume":"1","author":"EA Lee","year":"2016","unstructured":"Lee, E.A.: Fundamental limits of cyber-physical systems modeling. ACM Trans. Cyber-Phys. Syst. 1(1), 1\u201326 (2016)","journal-title":"ACM Trans. Cyber-Phys. Syst."},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Computing and Software Science: State of the Art and Perspectives, pp. 478\u2013504. Springer, Cham (2019)","DOI":"10.1007\/978-3-319-91908-9_23"},{"issue":"5s","key":"1_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3609134","volume":"22","author":"S Lin","year":"2023","unstructured":"Lin, S., et al.: Towards building verifiable CPS using lingua franca. ACM Trans. Embed. Comput. Syst. 22(5s), 1\u201324 (2023)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: International Colloquium on Automata, Languages, and Programming, pp. 652\u2013671. Springer, Cham (1989)","DOI":"10.1007\/BFb0035790"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Putnik, G.D., Ferreira, L., Lopes, N., Putnik, Z.: What is a cyber-physical system: definitions and models spectrum. FME Trans. 47(4) (2019)","DOI":"10.5937\/fmet1904663P"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Qin, X., Xia, Y., Zutshi, A., Fan, C., Deshmukh, J.V.: Statistical verification of cyber-physical systems using surrogate models and conformal inference. In: 2022 ACM\/IEEE 13th International Conference on Cyber-Physical Systems (ICCPS), pp. 116\u2013126. IEEE (2022)","DOI":"10.1109\/ICCPS54341.2022.00017"},{"issue":"7","key":"1_CR31","doi-asserted-by":"publisher","first-page":"1068","DOI":"10.3390\/math8071068","volume":"8","author":"M Sirjani","year":"2020","unstructured":"Sirjani, M., Lee, E.A., Khamespanah, E.: Verification of cyberphysical systems. Mathematics 8(7), 1068 (2020)","journal-title":"Mathematics"},{"key":"1_CR32","unstructured":"Sutton, R.S.: Reinforcement Learning: An Introduction. A Bradford Book (2018)"},{"key":"1_CR33","unstructured":"UPPAAL: UPPAAL documentation. https:\/\/docs.uppaal.org\/"},{"key":"1_CR34","unstructured":"Wired: Hackers remotely kill a jeep on the highwaywith me in it (2015). https:\/\/www.wired.com\/2015\/07\/hackers-remotely-kill-jeep-highway\/"}],"container-title":["Lecture Notes in Computer Science","Rebeca for Actor Analysis in Action"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-85134-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,1]],"date-time":"2025-04-01T08:35:00Z","timestamp":1743496500000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-85134-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031851339","9783031851346"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-85134-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"21 March 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}