{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:14:36Z","timestamp":1762863276935,"version":"3.40.3"},"publisher-location":"Cham","reference-count":66,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656323"},{"type":"electronic","value":"9783031656330"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Cyber-physical systems (CPSs) are used in many safety-critical areas, making it crucial to ensure their safety. However, with CPSs increasingly dynamically deployed and reconfigured during runtime, their safety analysis becomes challenging. For one thing, reconfigurable CPSs usually consist of multiple agents dynamically connected during runtime. Their highly dynamic system topologies are too intricate for traditional modeling languages, which, in turn, hinders formal analysis. For another, due to the growing size and uncertainty of reconfigurable CPSs, their system models can be huge and even unavailable at design time. This calls for runtime analysis approaches with better scalability and efficiency. To address these challenges, we propose a scenario-based hierarchical modeling language for reconfigurable CPS. It provides template models for agent inherent features, together with an instantiation mechanism to activate single agent\u2019s runtime behavior, communication configurations for multiple agents\u2019 connected behaviors, and scenario task configurations for their dynamic topologies. We also present a path-oriented falsification approach to falsify system requirements. It employs classification-model-based optimization to explore search space effectively and cut unnecessary system simulations and robustness calculations for efficiency. Our modeling and falsification are implemented in a tool called . Experiments have shown that it can largely reduce modeling time and improve modeling accuracy, and perform scalable CPS falsification with high success rates in seconds.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_15","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"329-355","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Scenario-Based Flexible Modeling and\u00a0Scalable Falsification for\u00a0Reconfigurable CPSs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6170-5675","authenticated-orcid":false,"given":"Jiawan","family":"Wang","sequence":"first","affiliation":[]},{"given":"Wenxia","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Muzimiao","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Jiaqi","family":"Wei","sequence":"additional","affiliation":[]},{"given":"Yuhui","family":"Shi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0517-7801","authenticated-orcid":false,"given":"Lei","family":"Bu","sequence":"additional","affiliation":[]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Acharya, S., Bharadwaj, A., Simmhan, Y., Gopalan, A., Parag, P., Tyagi, H.: Cornet: A co-simulation middleware for robot networks. In: 2020 International Conference on COMmunication Systems & NETworkS (COMSNETS), pp. 245\u2013251. IEEE (2020)","DOI":"10.1109\/COMSNETS48256.2020.9027459"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Ahmadi, A., Moradi, M., Cherifi, C., Cheutet, V., Ouzrout, Y.: Wireless connectivity of cps for smart manufacturing: a survey. In: 2018 12th International Conference on Software, Knowledge, Information Management & Applications (SKIMA), pp.\u00a01\u20138. IEEE (2018)","DOI":"10.1109\/SKIMA.2018.8631535"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-319-95582-7_27","volume-title":"Formal Methods","author":"T Akazaki","year":"2018","unstructured":"Akazaki, T., Liu, S., Yamagata, Y., Duan, Y., Hao, J.: Falsification of cyber-physical systems using deep reinforcement learning. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 456\u2013465. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_27"},{"key":"15_CR4","unstructured":"Alur, R.: Principles of cyber-physical systems. MIT press (2015)"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., et al.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theoret. Comput. Sci."},{"issue":"1\u20132","key":"15_CR6","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.jlap.2005.10.004","volume":"68","author":"R Alur","year":"2006","unstructured":"Alur, R., Grosu, R., Lee, I., Sokolsky, O.: Compositional modeling and refinement for hierarchical hybrid systems. J. Logic Algebraic Program. 68(1\u20132), 105\u2013128 (2006)","journal-title":"J. Logic Algebraic Program."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Annapureddy, Y.S.R., Fainekos, G.E.: Ant colonies for temporal logic falsification of hybrid systems. In: IECON 2010-36th Annual Conference on IEEE Industrial Electronics Society, pp. 91\u201396. IEEE (2010)","DOI":"10.1109\/IECON.2010.5675195"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_21"},{"key":"15_CR9","unstructured":"Audemard, G., Simon, L.: Glucose: a solver that predicts learnt clauses quality. SAT Competition pp.\u00a07\u20138 (2009)"},{"issue":"3","key":"15_CR10","doi-asserted-by":"publisher","first-page":"1273","DOI":"10.3390\/en16031273","volume":"16","author":"G Bazyd\u0142o","year":"2023","unstructured":"Bazyd\u0142o, G.: Designing reconfigurable cyber-physical systems using unified modeling language. Energies 16(3), 1273 (2023)","journal-title":"Energies"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"B\u00e9rard, B., et al.: Systems and software verification: model-checking techniques and tools. Springer Science & Business Media (2013)","DOI":"10.1002\/9781118558188.ch2"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Bergstra, J.A., Middelburg, C.A.: Process algebra for hybrid systems. Theoret. Comput. Sci. 335(2-3), 215\u2013280 (2005)","DOI":"10.1016\/j.tcs.2004.04.019"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Bersani, M.M., Garc\u00eda-Valls, M.: Online verification in cyber-physical systems: Practical bounds for meaningful temporal costs. J. Softw. Evolution Proc. 30(3) (2018)","DOI":"10.1002\/smr.1880"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Bogomolov, S., Frehse, G., Gurung, A., Li, D., Martius, G., Ray, R.: Falsification of hybrid systems using symbolic reachability and trajectory splicing. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201310 (2019)","DOI":"10.1145\/3302504.3311813"},{"issue":"1","key":"15_CR15","doi-asserted-by":"publisher","first-page":"325","DOI":"10.3182\/20050703-6-CZ-1902.00338","volume":"38","author":"E Brinksma","year":"2005","unstructured":"Brinksma, E., Krilavi\u0109ius, T., Usenko, Y.S.: Process algebraic approach to hybrid systems. IFAC Proc. Vol. 38(1), 325\u2013330 (2005)","journal-title":"IFAC Proc. Vol."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Li, X.: Bach: bounded reachability checker for linear hybrid automata. In: 2008 Formal Methods in Computer-Aided Design, pp.\u00a01\u20134. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Cavalcante, E., Batista, T., Oquendo, F.: Supporting dynamic software architectures: From architectural description to implementation. In: 2015 12th Working IEEE\/IFIP Conference on Software Architecture, pp. 31\u201340. IEEE (2015)","DOI":"10.1109\/WICSA.2015.21"},{"key":"15_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"15_CR19","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R., et\u00a0al.: Handbook of model checking, vol.\u00a010. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F Copty","year":"2001","unstructured":"Copty, F., et al.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436\u2013453. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_43"},{"key":"15_CR21","unstructured":"Cotton, S., Frehse, G., Lebeltel, O.: The spaceex modeling language. SpaceEx tool (2010)"},{"issue":"2","key":"15_CR22","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.jlap.2004.02.001","volume":"62","author":"PJL Cuijpers","year":"2005","unstructured":"Cuijpers, P.J.L., Reniers, M.A.: Hybrid process algebra. J. Logic Algebraic Program. 62(2), 191\u2013245 (2005)","journal-title":"J. Logic Algebraic Program."},{"key":"15_CR23","doi-asserted-by":"crossref","unstructured":"Dafflon, B., Moalla, N., Ouzrout, Y.: The challenges, approaches, and used techniques of cps for manufacturing in industry 4.0: a literature review. Inter. J. Adv. Manufact. Technol. 113, 2395\u20132412 (2021)","DOI":"10.1007\/s00170-020-06572-4"},{"key":"15_CR24","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/s10703-009-0066-0","volume":"34","author":"T Dang","year":"2009","unstructured":"Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Design 34, 183\u2013213 (2009)","journal-title":"Formal Methods Syst. Design"},{"issue":"5s","key":"15_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3126521","volume":"16","author":"J Deshmukh","year":"2017","unstructured":"Deshmukh, J., Horvat, M., Jin, X., Majumdar, R., Prabhu, V.S.: Testing cyber-physical systems through bayesian optimization. ACM Trans. Embedded Comput. Syst. (TECS) 16(5s), 1\u201318 (2017)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"issue":"27","key":"15_CR26","first-page":"e3","volume":"8","author":"HT Do","year":"2021","unstructured":"Do, H.T., et al.: Formation control algorithms for multiple-uavs: a comprehensive survey. EAI Endorsed Trans. Indus. Netw. Intell. Syst. 8(27), e3\u2013e3 (2021)","journal-title":"EAI Endorsed Trans. Indus. Netw. Intell. Syst."},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_17"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Frehse, G.: Modular, hierarchical models of control systems in spaceex. In: 2013 European Control Conference (ECC), pp. 4244\u20134251. IEEE (2013)","DOI":"10.23919\/ECC.2013.6669815"},{"key":"15_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-642-15297-9_9","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92\u2013106. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_9"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Handbook of Model Checking, pp. 1047\u20131110 (2018)","DOI":"10.1007\/978-3-319-10575-8_30"},{"key":"15_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-17524-9_10","volume-title":"NASA Formal Methods","author":"T Dreossi","year":"2015","unstructured":"Dreossi, T., Dang, T., Donz\u00e9, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127\u2013142. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_10"},{"issue":"5","key":"15_CR32","doi-asserted-by":"publisher","first-page":"5192","DOI":"10.1109\/JESTPE.2020.2981921","volume":"9","author":"Y Du","year":"2020","unstructured":"Du, Y., Lu, X., Wang, J., Chen, B., Tu, H., Lukic, S.: Dynamic microgrids in resilient distribution systems with reconfigurable cyber-physical networks. IEEE J. Emerging Selected Topics Power Electr. 9(5), 5192\u20135205 (2020)","journal-title":"IEEE J. Emerging Selected Topics Power Electr."},{"key":"15_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-030-30281-8_10","volume-title":"Quantitative Evaluation of Systems","author":"G Ernst","year":"2019","unstructured":"Ernst, G., Sedwards, S., Zhang, Z., Hasuo, I.: Fast falsification of hybrid systems using probabilistically adaptive input. In: Parker, D., Wolf, V. (eds.) QEST 2019. LNCS, vol. 11785, pp. 165\u2013181. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30281-8_10"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Sankaranarayanan, S., Ueda, K., Yazarel, H.: Verification of automotive control applications using s-taliro. In: 2012 American Control Conference (ACC), pp. 3567\u20133572. IEEE (2012)","DOI":"10.1109\/ACC.2012.6315384"},{"key":"15_CR35","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: Phaver: algorithmic verification of hybrid systems past hytech. Int. J. Softw. Tools Technol. Transfer 10, 263\u2013279 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Gray, J., Rumpe, B.: Modeling dynamic structures (2020)","DOI":"10.1007\/s10270-020-00793-7"},{"key":"15_CR38","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278\u2013292. IEEE (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Hu, Y.Q., Qian, H., Yu, Y.: Sequential classification-based optimization for direct policy search. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a031 (2017)","DOI":"10.1609\/aaai.v31i1.10927"},{"issue":"4","key":"15_CR40","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1109\/MIC.2004.6","volume":"8","author":"MP Huget","year":"2004","unstructured":"Huget, M.P.: Agent uml notation for multiagent system design. IEEE Internet Comput. 8(4), 63\u201371 (2004)","journal-title":"IEEE Internet Comput."},{"issue":"3","key":"15_CR41","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"},{"key":"15_CR42","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to embedded systems: A cyber-physical systems approach. MIT press (2016)"},{"key":"15_CR43","doi-asserted-by":"publisher","unstructured":"Li, Y., Zhu, H., Braught, K., Shen, K., Mitra, S.: Verse: a python library for reasoning about multi-agent hybrid system scenarios. In: International Conference on Computer Aided Verification, pp. 351\u2013364. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_18","DOI":"10.1007\/978-3-031-37706-8_18"},{"issue":"1","key":"15_CR44","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/TAC.2002.806650","volume":"48","author":"J Lygeros","year":"2003","unstructured":"Lygeros, J., Johansson, K.H., Simic, S.N., Zhang, J., Sastry, S.S.: Dynamical properties of hybrid automata. IEEE Trans. Autom. Control 48(1), 2\u201317 (2003)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"15_CR45","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Hybrid i\/o automata. Inform. Comput. 185(1), 105\u2013157 (2003)","journal-title":"Inform. Comput."},{"key":"15_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"15_CR47","doi-asserted-by":"crossref","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. Pillars of Computer Science: Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, pp. 475\u2013505 (2008)","DOI":"10.1007\/978-3-540-78127-1_26"},{"key":"15_CR48","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10898-020-00937-5","volume":"79","author":"L Mathesen","year":"2021","unstructured":"Mathesen, L., Pedrielli, G., Ng, S.H., Zabinsky, Z.B.: Stochastic optimization with adaptive restart: a framework for integrated local and global learning. J. Global Optim. 79, 87\u2013110 (2021)","journal-title":"J. Global Optim."},{"key":"15_CR49","doi-asserted-by":"crossref","unstructured":"Mathesen, L., Yaghoubi, S., Pedrielli, G., Fainekos, G.: Falsification of cyber-physical systems with robustness uncertainty quantification through stochastic optimization with adaptive restart. In: 2019 IEEE 15th International Conference on Automation Science and Engineering (CASE), pp. 991\u2013997. IEEE (2019)","DOI":"10.1109\/COASE.2019.8843005"},{"key":"15_CR50","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-14843-9_4","volume-title":"Programming Multi-Agent Systems","author":"A Mohammed","year":"2010","unstructured":"Mohammed, A., Furbach, U.: Multi-agent systems: modeling and verification using hybrid automata. In: Braubach, L., Briot, J.-P., Thangarajah, J. (eds.) ProMAS 2009. LNCS (LNAI), vol. 5919, pp. 49\u201366. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14843-9_4"},{"key":"15_CR51","unstructured":"Mohammed, A., Stolzenburg, F.: Implementing hierarchical hybrid automata using constraint logic programming. In: Proceedings of 22nd Workshop on (Constraint) Logic Programming, Dresden, pp. 60\u201371 (2008)"},{"key":"15_CR52","doi-asserted-by":"crossref","unstructured":"Nghiem, T., Sankaranarayanan, S., Fainekos, G., Ivanci\u0107, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 211\u2013220 (2010)","DOI":"10.1145\/1755952.1755983"},{"issue":"2","key":"15_CR53","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10703-008-0058-5","volume":"34","author":"E Plaku","year":"2009","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification by combining motion planning and discrete search. Formal Methods Syst. Design 34(2), 157\u2013182 (2009)","journal-title":"Formal Methods Syst. Design"},{"key":"15_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-24743-2_32","volume-title":"Hybrid Systems: Computation and Control","author":"S Prajna","year":"2004","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477\u2013492. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24743-2_32"},{"issue":"8","key":"15_CR55","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415\u20131428 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"15_CR56","unstructured":"Rosu, G., Havelund, K.: Synthesizing dynamic programming algorithms from linear temporal logic formulae (2001)"},{"key":"15_CR57","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Fainekos, G.: Falsification of temporal properties of hybrid systems using the cross-entropy method. In: Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control, pp. 125\u2013134 (2012)","DOI":"10.1145\/2185632.2185653"},{"issue":"3","key":"15_CR58","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/s10270-021-00875-0","volume":"20","author":"B Seli\u0107","year":"2021","unstructured":"Seli\u0107, B.: Specifying dynamic software system architectures. Softw. Syst. Model. 20(3), 595\u2013605 (2021)","journal-title":"Softw. Syst. Model."},{"key":"15_CR59","doi-asserted-by":"crossref","unstructured":"Sha, L., Gopalakrishnan, S., Liu, X., Wang, Q.: Cyber-physical systems: A new frontier. In: 2008 IEEE International Conference on Sensor Networks, Ubiquitous, and Trustworthy Computing (Sutc 2008), pp.\u00a01\u20139. IEEE (2008)","DOI":"10.1109\/SUTC.2008.85"},{"key":"15_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02777-2_24"},{"key":"15_CR61","doi-asserted-by":"crossref","unstructured":"Waga, M.: Falsification of cyber-physical systems with robustness-guided black-box checking. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, pp. 1\u201313 (2020)","DOI":"10.1145\/3365365.3382193"},{"issue":"1","key":"15_CR62","first-page":"30","volume":"2","author":"K Wan","year":"2011","unstructured":"Wan, K., Hughes, D., Man, K.L., Krilavicius, T., Zou, S.: Investigation on composition mechanisms for cyber physical systems. Inter. J. Design, Anal. Tools Integrated Circ. Syst. 2(1), 30 (2011)","journal-title":"Inter. J. Design, Anal. Tools Integrated Circ. Syst."},{"issue":"2","key":"15_CR63","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1109\/TCAD.2021.3056360","volume":"41","author":"J Wang","year":"2021","unstructured":"Wang, J., Bu, L., Xing, S., Li, X.: Path-oriented, derivative-free approach for safety falsification of nonlinear and nondeterministic cps. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(2), 238\u2013251 (2021)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"15_CR64","doi-asserted-by":"crossref","unstructured":"Yu, Y., Qian, H., Hu, Y.Q.: Derivative-free optimization via classification. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a030 (2016)","DOI":"10.1609\/aaai.v30i1.10289"},{"issue":"11","key":"15_CR65","doi-asserted-by":"publisher","first-page":"2894","DOI":"10.1109\/TCAD.2018.2858463","volume":"37","author":"Z Zhang","year":"2018","unstructured":"Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., Hasuo, I.: Two-layered falsification of hybrid systems guided by monte carlo tree search. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(11), 2894\u20132905 (2018)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"15_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1007\/978-3-030-81685-8_29","volume-title":"Computer Aided Verification","author":"Z Zhang","year":"2021","unstructured":"Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J.: Effective hybrid system falsification using monte carlo tree search guided by QB-robustness. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 595\u2013618. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_29"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65633-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:14:57Z","timestamp":1732479297000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}