{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T13:05:54Z","timestamp":1760101554925,"version":"3.40.4"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906428","type":"print"},{"value":"9783031906435","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. We present our tool <jats:sc>SemML<\/jats:sc>, which won this year\u2019s LTL realizability tracks of <jats:sc>SYNTCOMP<\/jats:sc>, after years of domination by <jats:sc>Strix<\/jats:sc>. While both tools are based on the automata-theoretic approach, ours relies heavily on (i)  <jats:sc>Sem<\/jats:sc>\n            <jats:italic>antic labelling<\/jats:italic>, additional information of logical nature, coming from recent LTL-to-automata translations and decorating the resulting parity game, and (ii)  <jats:sc>M<\/jats:sc>\n            <jats:italic>achine-<\/jats:italic>\n            <jats:sc>L<\/jats:sc>\n            <jats:italic>earning<\/jats:italic> approaches turning this information into a guidance oracle for on-the-fly exploration of the parity game (whence the name <jats:sc>SemML<\/jats:sc>). Our tool fills the missing gaps of previous suggestions to use such an oracle and provides an efficient implementation with additional algorithmic improvements. We evaluate <jats:sc>SemML<\/jats:sc> both on the entire set of SYNTCOMP as well as a synthetic data set, compare it to <jats:sc>Strix<\/jats:sc>, and analyze the advantages and limitations. As <jats:sc>SemML<\/jats:sc> solves more instances on SYNTCOMP and does so significantly faster on larger instances, this demonstrates for the first time that machine-learning-aided approaches can out-perform state-of-the-art tools in real LTL synthesis.<\/jats:p>","DOI":"10.1007\/978-3-031-90643-5_12","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:07Z","timestamp":1745993287000},"page":"233-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-2165","authenticated-orcid":false,"given":"Tobias","family":"Meggendorfer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6512-8693","authenticated-orcid":false,"given":"Maximilian","family":"Prokop","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9510-5485","authenticated-orcid":false,"given":"Ashkan","family":"Zarkhah","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"12_CR1","unstructured":"The reactive synthesis competition: SYNTCOMP 2018 results. http:\/\/www.syntcomp.org\/syntcomp-2018-results\/ (2018), http:\/\/www.syntcomp.org\/syntcomp-2018-results\/"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Torre, S.L.: Deterministic generators and games for ltl fragments. ACM Trans. Comput. Log. 5(1), 1\u201325 (2004). https:\/\/doi.org\/10.1145\/963927.963928","DOI":"10.1145\/963927.963928"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Bansal, S., Giacomo, G.D., Stasio, A.D., Li, Y., Vardi, M.Y., Zhu, S.: Compositional safety LTL synthesis. In: Lal, A., Tonetta, S. (eds.) Verified Software. Theories, Tools and Experiments - 14th International Conference, VSTTE 2022, Trento, Italy, October 17-18, 2022, Revised Selected Papers. Lecture Notes in Computer Science, vol. 13800, pp. 1\u201319. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-25803-9_1, https:\/\/doi.org\/10.1007\/978-3-031-25803-9_1","DOI":"10.1007\/978-3-031-25803-9_1"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol.\u00a07358, pp. 652\u2013657. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"12_CR5","unstructured":"B\u00fcchi, J.: On a decision method in restricted second-order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Proceedings of the First International Congress on Logic, Methodology, and Philosophy of Science 1960 (1962)"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Cadilhac, M., P\u00e9rez, G.A.: Acacia-bonsai: A modern implementation of downset-based LTL realizability. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13994, pp. 192\u2013207. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_14","DOI":"10.1007\/978-3-031-30820-8_14"},{"key":"12_CR7","unstructured":"Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. Journal of Symbolic Logic (1963)"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Omar, A., Schmitt, F.: Neurosynt: A neuro-symbolic portfolio solver for reactive synthesis. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14572, pp. 45\u201367. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_3","DOI":"10.1007\/978-3-031-57256-2_3"},{"key":"12_CR9","unstructured":"Cosler, M., Schmitt, F., Hahn, C., Finkbeiner, B.: Iterative circuit repair against formal specifications. In: The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net (2023), https:\/\/openreview.net\/forum?id=SEcSahl0Ql"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice. p. 7\u201315. FMSP \u201998, Association for Computing Machinery, New York, NY, USA (1998). https:\/\/doi.org\/10.1145\/298595.298598","DOI":"10.1145\/298595.298598"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Ehlers, R.: Unbeast: Symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06605, pp. 272\u2013275. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25","DOI":"10.1007\/978-3-642-19835-9_25"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Raskin, J., Sickert, S.: From linear temporal logic and limit-deterministic b\u00fcchi automata to deterministic parity automata. Int. J. Softw. Tools Technol. Transf. 24(4), 635\u2013659 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00663-1","DOI":"10.1007\/s10009-022-00663-1"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6), 33:1\u201333:61 (2020). https:\/\/doi.org\/10.1145\/3417995","DOI":"10.1145\/3417995"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: An experimentation framework for bounded synthesis. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10427, pp. 325\u2013332. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Piskac, R., Dimitrova, R. (eds.) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17-18, 2016. EPTCS, vol.\u00a0229, pp. 112\u2013132 (2016). https:\/\/doi.org\/10.4204\/EPTCS.229.10","DOI":"10.4204\/EPTCS.229.10"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Jacobs, S., P\u00e9rez, G.A., Abraham, R., Bruy\u00e8re, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, K.J., Michaud, T., Pommellet, A., Renkin, F., Schlehuber-Caissier, P., Sakr, M., Sickert, S., Staquet, G., Tamines, C., Tentrup, L., Walker, A.: The reactive synthesis competition (SYNTCOMP): 2018-2021. CoRR abs\/2206.00251 (2022). https:\/\/doi.org\/10.48550\/arXiv.2206.00251","DOI":"10.48550\/arXiv.2206.00251"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer-Aided Design, 6th International Conference, FMCAD 2006, San Jose, California, USA, November 12-16, 2006, Proceedings. pp. 117\u2013124. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/FMCAD.2006.22","DOI":"10.1109\/FMCAD.2006.22"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Esparza, J.: Deterministic automata for the (f, g)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings. Lecture Notes in Computer Science, vol.\u00a07358, pp. 7\u201322. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_7","DOI":"10.1007\/978-3-642-31424-7_7"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Manta, A., Meggendorfer, T.: Semantic labelling and learning for parity game solving in LTL synthesis. In: Chen, Y., Cheng, C., Esparza, J. (eds.) Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11781, pp. 404\u2013422. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_24","DOI":"10.1007\/978-3-030-31784-3_24"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Prokop, M., Rieder, S.: Guessing winning policies in LTL synthesis by semantic learning. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13964, pp. 390\u2013414. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_20","DOI":"10.1007\/978-3-031-37706-8_20"},{"key":"12_CR21","unstructured":"Kretinsky, J., Meggendorfer, T., Prokop, M., Zarkhah, A.: Semml: Enhancing automata-theoretic ltl synthesis with machine learning (2025), https:\/\/arxiv.org\/abs\/2501.17496"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: A library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11138, pp. 543\u2013550. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34","DOI":"10.1007\/978-3-030-01090-4_34"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S., Ziegler, C.: Rabinizer 4: From LTL to your favourite deterministic automaton. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 567\u2013577. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_30","DOI":"10.1007\/978-3-319-96145-3_30"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04144, pp. 31\u201344. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_6","DOI":"10.1007\/11817963_6"},{"key":"12_CR25","unstructured":"Meggendorfer, T.: JBDD: A java BDD library. https:\/\/github.com\/incaseoftrouble\/jbdd (2017)"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 578\u2013586. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"12_CR27","unstructured":"Pedregosa, F., Varoquaux, G., Gramfort, A., Michel, V., Thirion, B., Grisel, O., Blondel, M., Prettenhofer, P., Weiss, R., Dubourg, V., Vanderplas, J., Passos, A., Cournapeau, D., Brucher, M., Perrot, M., Duchesnay, E.: Scikit-learn: Machine learning in Python. Journal of Machine Learning Research 12, 2825\u20132830 (2011)"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic buchi and streett automata to deterministic parity automata. In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings. pp. 255\u2013264. IEEE Computer Society (2006). https:\/\/doi.org\/10.1109\/LICS.2006.28","DOI":"10.1109\/LICS.2006.28"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a03855, pp. 364\u2013380. Springer (2006). https:\/\/doi.org\/10.1007\/11609773_24","DOI":"10.1007\/11609773_24"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. pp. 46\u201357. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings. Lecture Notes in Computer Science, vol.\u00a0372, pp. 652\u2013671. Springer (1989). https:\/\/doi.org\/10.1007\/BFb0035790","DOI":"10.1007\/BFb0035790"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Prokop, M.: Artifact for \"semml: Enhancing automata-theoretic ltl synthesis with machine learning\" (Jan 2025). https:\/\/doi.org\/10.5281\/zenodo.14587814, https:\/\/doi.org\/10.5281\/zenodo.14587814","DOI":"10.5281\/zenodo.14587814"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., Pommellet, A.: Dissecting ltlsynt. Formal Methods Syst. Des. 61(2), 248\u2013289 (2022). https:\/\/doi.org\/10.1007\/S10703-022-00407-6","DOI":"10.1007\/S10703-022-00407-6"},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Rodr\u00edguez, A., S\u00e1nchez, C.: Boolean abstractions for realizability modulo theories. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 305\u2013328. Springer Nature Switzerland, Cham (2023)","DOI":"10.1007\/978-3-031-37709-9_15"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988. pp. 319\u2013327. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Schewe, S.: Tighter bounds for the determinisation of b\u00fcchi automata. In: de\u00a0Alfaro, L. (ed.) Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05504, pp. 167\u2013181. Springer (2009).https:\/\/doi.org\/10.1007\/978-3-642-00596-1_13","DOI":"10.1007\/978-3-642-00596-1_13"},{"key":"12_CR37","unstructured":"Schmitt, F., Hahn, C., Rabe, M.N., Finkbeiner, B.: Neural circuit synthesis from specification patterns. In: Ranzato, M., Beygelzimer, A., Dauphin, Y.N., Liang, P., Vaughan, J.W. (eds.) Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual. pp. 15408\u201315420 (2021), https:\/\/proceedings.neurips.cc\/paper\/2021\/hash\/8230bea7d54bcdf99cdfe85cb07313d5-Abstract.html"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Sickert, S., Esparza, J., Jaax, S., K\u0159et\u00ednsk\u00fd, J.: Limit-deterministic b\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a09780, pp. 312\u2013332. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17","DOI":"10.1007\/978-3-319-41540-6_17"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 95, 12th Annual Symposium on Theoretical Aspects of Computer Science, Munich, Germany, March 2-4, 1995, Proceedings. Lecture Notes in Computer Science, vol.\u00a0900, pp. 1\u201313. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-59042-0_57","DOI":"10.1007\/3-540-59042-0_57"},{"key":"12_CR40","doi-asserted-by":"publisher","unstructured":"Tomita, T., Ueno, A., Shimakawa, M., Hagihara, S., Yonezaki, N.: Safraless LTL synthesis considering maximal realizability. Acta Informatica 54(7), 655\u2013692 (2017). https:\/\/doi.org\/10.1007\/S00236-016-0280-3","DOI":"10.1007\/S00236-016-0280-3"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90643-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:08:11Z","timestamp":1745993291000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90643-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906428","9783031906435"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90643-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","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":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}