{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:08Z","timestamp":1776333488557,"version":"3.51.2"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656323","type":"print"},{"value":"9783031656330","type":"electronic"}],"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>Techniques of light-weight formal methods, such as monitoring and falsification, are attracting attention for quality assurance of cyber-physical systems. The techniques require formal specs, however, and writing right specs is still a practical challenge. Commonly one relies on<jats:italic>trace synthesis<\/jats:italic>\u2014i.e. automatic generation of a signal that satisfies a given spec\u2014to examine the meaning of a spec. In this work, motivated by 1) complex STL specs from an automotive safety standard and 2) the struggle of existing tools in their trace synthesis, we introduce a novel trace synthesis algorithm for STL specs. It combines the use of MILP (inspired by works on controller synthesis) and a<jats:italic>variable-interval encoding<\/jats:italic>of STL semantics (previously studied for SMT-based STL model checking). The algorithm solves model checking, too, as the dual of trace synthesis. Our experiments show that only ours has realistic performance needed for the interactive examination of STL specs by trace synthesis.<\/jats:p>","DOI":"10.1007\/978-3-031-65633-0_13","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"282-306","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Optimization-Based Model Checking and\u00a0Trace Synthesis for\u00a0Complex STL Specifications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7147-3989","authenticated-orcid":false,"given":"Sota","family":"Sato","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9260-9697","authenticated-orcid":false,"given":"Jie","family":"An","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-9846","authenticated-orcid":false,"given":"Zhenya","family":"Zhang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"13_CR1","unstructured":"ForeSee falsification solver (2021). https:\/\/github.com\/choshina\/ForeSee"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-319-21668-3_21","volume-title":"Computer Aided Verification","author":"T Akazaki","year":"2015","unstructured":"Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid system falsification. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 356\u2013374. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_21"},{"issue":"1","key":"13_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996). https:\/\/doi.org\/10.1145\/227595.227602","journal-title":"J. ACM"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-29860-8_12","volume-title":"Runtime Verification","author":"E Asarin","year":"2012","unstructured":"Asarin, E., Donz\u00e9, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 147\u2013160. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_12"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Asghari, M., Fathollahi-Fard, A.M., Mirzapour Al-e hashem, S.M.J., Dulebenets, M.A.: Transformation and linearization techniques in optimization: a state-of-the-art survey. Mathematics 10(2), 283 (2022). https:\/\/doi.org\/10.3390\/math10020283","DOI":"10.3390\/math10020283"},{"key":"13_CR6","unstructured":"Atkinson, K.E.: An Introduction to Numerical Analysis. Wiley, New York, second edn. (1989). http:\/\/www.worldcat.org\/isbn\/0471500232"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using syntactic separation. Proc. ACM Program. Lang. 3(POPL), 51:1\u201351:30 (2019). https:\/\/doi.org\/10.1145\/3290364","DOI":"10.1145\/3290364"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-75632-5_5","volume-title":"Lectures on Runtime Verification","author":"E Bartocci","year":"2018","unstructured":"Bartocci, E., et al.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135\u2013175. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5_5"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Mateis, C., Nesterini, E., Nickovic, D.: Survey on mining signal temporal logic specifications. Inf. Comput. 289(Part), 104957 (2022). https:\/\/doi.org\/10.1016\/J.IC.2022.104957","DOI":"10.1016\/J.IC.2022.104957"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Bu, L., Frehse, G., Kundu, A., Ray, R., Shi, Y., Zaffanella, E.: Arch-comp22 category report: Hybrid systems with piecewise constant dynamics and bounded model checking. In: Frehse, G., Althoff, M., Schoitsch, E., Guiochet, J. (eds.) Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22). EPiC Series in Computing, vol.\u00a090, pp. 44\u201357. EasyChair (2022). https:\/\/doi.org\/10.29007\/lnzf","DOI":"10.29007\/lnzf"},{"key":"13_CR11","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":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-642-39799-8_19","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2013","unstructured":"Donz\u00e9, A., Ferr\u00e8re, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264\u2013279. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_19"},{"key":"13_CR13","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":"13_CR14","doi-asserted-by":"publisher","unstructured":"Donz\u00e9, A., Raman, V.: BluSTL: controller synthesis from signal temporal logic specifications. In: ARCH14-15. 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, pp. 160\u2013150. https:\/\/doi.org\/10.29007\/g39q","DOI":"10.29007\/g39q"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: 2011 IEEE\/ACM Second International Conference on Cyber-Physical Systems, pp. 22\u201331. IEEE (2011). https:\/\/doi.org\/10.1109\/ICCPS.2011.24","DOI":"10.1109\/ICCPS.2011.24"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Ernst, G., et al.: ARCH-COMP 2021 category report: falsification with validation of results. In: Frehse, G., Althoff, M. (eds.) 8th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021. EPiC Series in Computing, vol.\u00a080, pp. 133\u2013152. EasyChair (2021). https:\/\/doi.org\/10.29007\/XWL1","DOI":"10.29007\/XWL1"},{"issue":"42","key":"13_CR17","doi-asserted-by":"publisher","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","journal-title":"Theoret. Comput. Sci."},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Glover, F.: Improved linear integer programming formulations of nonlinear integer problems. Manag. Sci. 22, 455\u2013460 (1975). https:\/\/doi.org\/10.1287\/mnsc.22.4.455","DOI":"10.1287\/mnsc.22.4.455"},{"issue":"2","key":"13_CR19","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1137\/110836183","volume":"23","author":"A Gupte","year":"2013","unstructured":"Gupte, A., Ahmed, S., Cheon, M.S., Dey, S.: Solving mixed integer bilinear problems using MILP formulations. SIAM J. Optim. 23(2), 721\u2013744 (2013). https:\/\/doi.org\/10.1137\/110836183","journal-title":"SIAM J. Optim."},{"key":"13_CR20","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2023). https:\/\/www.gurobi.com"},{"key":"13_CR21","unstructured":"Road vehicles - Test scenarios for automated driving systems - Scenario based safety evaluation framework. Standard, International Organization for Standardization, Geneva, CH (2022)"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"1718","DOI":"10.1109\/LCSYS.2021.3132839","volume":"6","author":"V Kurtz","year":"2022","unstructured":"Kurtz, V., Lin, H.: A more scalable mixed-integer encoding for metric temporal logic. IEEE Control. Syst. Lett. 6, 1718\u20131723 (2022). https:\/\/doi.org\/10.1109\/LCSYS.2021.3132839","journal-title":"IEEE Control. Syst. Lett."},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Lee, J., Yu, G., Bae, K.: Efficient SMT-based model checking for signal temporal logic. In: 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 343\u2013354 (2021). https:\/\/doi.org\/10.1109\/ASE51524.2021.9678719","DOI":"10.1109\/ASE51524.2021.9678719"},{"key":"13_CR24","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":"13_CR25","doi-asserted-by":"publisher","unstructured":"Pedrielli, G., et al.: Part-X: A family of stochastic algorithms for search-based test generation with probabilistic guarantees. IEEE Trans. Autom. Sci. Eng. 1\u201322 (2023). https:\/\/doi.org\/10.1109\/TASE.2023.3297984","DOI":"10.1109\/TASE.2023.3297984"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Prabhakar, P., Lal, R., Kapinski, J.: Automatic trace generation for signal temporal logic. In: 2018 IEEE Real-Time Systems Symposium (RTSS), pp. 208\u2013217. IEEE, Nashville, TN (2018). https:\/\/doi.org\/10.1109\/RTSS.2018.00038","DOI":"10.1109\/RTSS.2018.00038"},{"issue":"5","key":"13_CR27","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1093\/logcom\/8.5.669","volume":"8","author":"AM Rabinovich","year":"1998","unstructured":"Rabinovich, A.M.: On the decidability of continuous time specification formalisms. J. Log. Comput. 8(5), 669\u2013678 (1998). https:\/\/doi.org\/10.1093\/logcom\/8.5.669","journal-title":"J. Log. Comput."},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Raman, V., Donz\u00e9, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Model predictive control with signal temporal logic specifications. In: 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles, CA, USA, December 15-17, 2014, pp. 81\u201387. IEEE (2014). https:\/\/doi.org\/10.1109\/CDC.2014.7039363","DOI":"10.1109\/CDC.2014.7039363"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Raman, V., Donz\u00e9, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis from signal temporal logic specifications. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, pp. 239\u2013248. ACM, Seattle Washington (2015). https:\/\/doi.org\/10.1145\/2728606.2728628","DOI":"10.1145\/2728606.2728628"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Reimann, J., et al.: Temporal logic formalisation of ISO 34502 critical scenarios: modular construction with the RSS safety distance. In: Proceedings of the 39th ACM\/SIGAPP Symposium on Applied Computing (SAC 2024) to appear (2024). arXiv:2403.18764","DOI":"10.1145\/3605098.3636014"},{"key":"13_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-319-63387-9_11","volume-title":"Computer Aided Verification","author":"H Roehm","year":"2017","unstructured":"Roehm, H., Heinz, T., Mayer, E.C.: STLInspector: STL Validation with Guarantees. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 225\u2013232. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_11"},{"key":"13_CR32","doi-asserted-by":"crossref","unstructured":"Sato, S., An, J., Zhang, Z., Hasuo, I.: Optimization-based model checking and trace synthesis for complex STL specifications (extended version) (2024). available on arXiv","DOI":"10.1007\/978-3-031-65633-0_13"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-642-05089-3_34","volume-title":"FM 2009: Formal Methods","author":"J Souyris","year":"2009","unstructured":"Souyris, J., Wiels, V., Delmas, D., Delseny, H.: Formal verification of avionics software products. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 532\u2013546. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-05089-3_34"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Yu, G., Lee, J., Bae, K.: Stlmc: Robust STL model checking of hybrid systems using SMT. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I. LNCS, vol. 13371, pp. 524\u2013537. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_26","DOI":"10.1007\/978-3-031-13185-1_26"},{"key":"13_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-030-90870-6_18","volume-title":"Formal Methods","author":"Z Zhang","year":"2021","unstructured":"Zhang, Z., Arcaini, P.: Gaussian process-based confidence estimation for hybrid system falsification. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 330\u2013348. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_18"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-030-25540-4_23","volume-title":"Computer Aided Verification","author":"Z Zhang","year":"2019","unstructured":"Zhang, Z., Hasuo, I., Arcaini, P.: Multi-armed bandits for Boolean connectives in hybrid system falsification. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 401\u2013420. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_23"},{"key":"13_CR37","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_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T20:14:44Z","timestamp":1732479284000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65633-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656323","9783031656330"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65633-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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"}}]}}