{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T03:59:26Z","timestamp":1783051166763,"version":"3.54.6"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Modern cyber-physical systems are complex, and requirements are often written in Signal Temporal Logic (STL). Writing the right STL is difficult in practice; engineers benefit from concrete executions that illustrate what a specification actually admits. Trace synthesis addresses this need, but a single witness rarely suffices to understand intent or explore edge cases\u2014diverse satisfying behaviors are far more informative. We introduce diversified trace synthesis: the automatic generation of sets of behaviorally diverse traces that satisfy a given STL formula. Building on a MILP encoding of STL and system model, we formalize three complementary diversification objectives\u2014Boolean distance, random Boolean distance, and value distance\u2014all captured by an objective function and solved iteratively. We implement these ideas in STLts-Div, a lightweight Python tool that integrates with Gurobi.<\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_1","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:27Z","timestamp":1779033087000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9912-3225","authenticated-orcid":false,"given":"Martin","family":"Jouve-Genty","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4260-8340","authenticated-orcid":false,"given":"Han","family":"Su","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7147-3989","authenticated-orcid":false,"given":"Sota","family":"Sato","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9260-9697","authenticated-orcid":false,"given":"Jie","family":"An","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3854-9846","authenticated-orcid":false,"given":"Zhenya","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"issue":"1","key":"1_CR1","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 (JACM) 43(1), 116\u2013146 (1996)","journal-title":"J. ACM (JACM)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Atkins, E.M., Bradley, J.M.: Aerospace cyber-physical systems education. In: AIAA Infotech@ Aerospace (I@ A) Conference, p.\u00a04809 (2013)","DOI":"10.2514\/6.2013-4809"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using syntactic separation. Proceedings of the ACM on Programming Languages, vol. 3(POPL), pp. 1\u201330 (2019)","DOI":"10.1145\/3290364"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Bu, L., Frehse, G., Kundu, A., Ray, R., Shi, Y., Zaffanella, E., et\u00a0al.: Arch-comp22 category report: hybrid systems with piecewise constant dynamics and bounded model checking. In: Proceedings of 9th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH22). EPiC Series in Computing, vol.\u00a090, pp. 44\u201357 (2022)","DOI":"10.29007\/lnzf"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Cheng, M., Zhou, Y., Xie, X.: Behavexplor: behavior diversity guided testing for autonomous driving systems. In: Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 488\u2013500 (2023)","DOI":"10.1145\/3597926.3598072"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Raman, V., Frehse, G., Althoff, M.: Blustl: controller synthesis from signal temporal logic specifications. ARCH@ CPSWeek 34, 160\u2013168 (2015)","DOI":"10.29007\/g39q"},{"key":"1_CR7","doi-asserted-by":"crossref","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)","DOI":"10.1109\/ICCPS.2011.24"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Ernst, G., et\u00a0al.: Arch-comp 2021 category report: Falsification with validation of results. In: ARCH@ ADHS, pp. 133\u2013152 (2021)","DOI":"10.29007\/xwl1"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theoret. Comput. Sci. 410(42), 4262\u20134291 (Sep2009). https:\/\/doi.org\/10.1016\/j.tcs.2009.06.021","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"1_CR10","unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2024). https:\/\/www.gurobi.com"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Jouve-Genty, M., Su, H., Sato, S., An, J., Zhang, Z., Hasuo, I.: STLts-Div: Diversified trace synthesis from STL specifications using MILP (Extended Version) (2025), available on arXiv","DOI":"10.1007\/978-3-032-26204-2_1"},{"key":"1_CR12","doi-asserted-by":"crossref","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. IEEE (2021)","DOI":"10.1109\/ASE51524.2021.9678719"},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1109\/LCSYS.2018.2853182","volume":"3","author":"L Lindemann","year":"2018","unstructured":"Lindemann, L., Dimarogonas, D.V.: Control barrier functions for signal temporal logic tasks. IEEE Control Syst. Lett. 3(1), 96\u2013101 (2018)","journal-title":"IEEE Control Syst. Lett."},{"key":"1_CR14","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":"1_CR15","doi-asserted-by":"crossref","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 (2018)","DOI":"10.1109\/RTSS.2018.00038"},{"issue":"5","key":"1_CR16","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)","journal-title":"J. Log. Comput."},{"key":"1_CR17","doi-asserted-by":"crossref","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 (2015)","DOI":"10.1145\/2728606.2728628"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Raman, V., Maasoumy, M., Donz\u00e9, A.: Model predictive control from signal temporal logic specifications: A case study. In: Proceedings of the 4th ACM SIGBED International Workshop on Design, Modeling, and Evaluation of Cyber-physical Systems, pp. 52\u201355 (2014)","DOI":"10.1145\/2593458.2593472"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Reimann, J., et\u00a0al.: 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, pp. 186\u2013195 (2024)","DOI":"10.1145\/3605098.3636014"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Sato, S., An, J., Zhang, Z., Hasuo, I.: Optimization-based model checking and trace synthesis for complex STL specifications, pp. 282\u2013306. Springer Nature Switzerland (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_13","DOI":"10.1007\/978-3-031-65633-0_13"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Su, H., Feng, S., Zhan, S., Zhan, N.: Switching controller synthesis for hybrid systems against stl formulas. In: International Symposium on Formal Methods, pp. 229\u2013247. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-71177-0_15","DOI":"10.1007\/978-3-031-71177-0_15"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Su, H., Shankar, S., Pinisetty, S., Roop, P.S., Zhan, N.: Runtime enforcement of cps against signal temporal logic. In: Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2025)","DOI":"10.1145\/3716863.3718052"},{"issue":"7","key":"1_CR23","doi-asserted-by":"publisher","first-page":"949","DOI":"10.1109\/5.871303","volume":"88","author":"CJ Tomlin","year":"2000","unstructured":"Tomlin, C.J., Lygeros, J., Sastry, S.S.: A game theoretic approach to controller design for hybrid systems. Proc. IEEE 88(7), 949\u2013970 (2000)","journal-title":"Proc. IEEE"},{"issue":"1","key":"1_CR24","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1049\/iet-syb:20070001","volume":"2","author":"P Ye","year":"2008","unstructured":"Ye, P., Entcheva, E., Smolka, S.A., Grosu, R.: Modelling excitable cells using cycle-linear hybrid automata. IET Syst. Biol. 2(1), 24\u201332 (2008)","journal-title":"IET Syst. Biol."},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Zhang, Z., An, J., Arcaini, P., Hasuo, I.: Online causation monitoring of signal temporal logic. In: International Conference on Computer Aided Verification, pp. 62\u201384. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_4","DOI":"10.1007\/978-3-031-37706-8_4"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T17:51:47Z","timestamp":1783014707000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}