{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T21:17:26Z","timestamp":1768339046486,"version":"3.49.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906527","type":"print"},{"value":"9783031906534","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>\n                    The goal of\n                    <jats:italic>logical controller synthesis<\/jats:italic>\n                    is to automatically compute a control strategy that regulates the discrete, event-driven behavior of a given plant s.t. a temporal logic specification holds over all remaining traces. Standard approaches to this problem construct a two-player game by composing a given complete plant model and the logical specification and applying standard algorithmic techniques to extract a control strategy. However, due to the often enormous state space of a complete plant model, this process can become computationally infeasible. In this paper, we introduce a novel synthesis approach that constructs a\n                    <jats:italic>universal controller<\/jats:italic>\n                    derived solely from the game obtained by the standard translation of the logical specification. The universal controller\u2019s moves are annotated with\n                    <jats:italic>prophecies<\/jats:italic>\n                    \u2013 predictions about the plant\u2019s behavior that ensure the move is safe. By evaluating these prophecies, the universal controller can be adapted to any plant over which the synthesis problem is realizable. This approach offers several key benefits, including enhanced scalability with respect to the plant\u2019s size, adaptability to changes in the plant, and improved explainability of the resulting control strategy. We also present encouraging experimental results obtained with our prototype tool,\n                    <jats:sc>unicon<\/jats:sc>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_9","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T07:51:37Z","timestamp":1746172297000},"page":"177-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Synthesis of Universal Safety Controllers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3184-6335","authenticated-orcid":false,"given":"Niklas","family":"Metzger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4407-8681","authenticated-orcid":false,"given":"Satya Prakash","family":"Nayak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2801-639X","authenticated-orcid":false,"given":"Anne-Kathrin","family":"Schmuck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Fsomegalib. https:\/\/github.com\/ravenbeutner\/FsOmegaLib, accessed: 2024-09-25","DOI":"10.5965\/1984723825572024009"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90224-P, https:\/\/doi.org\/10.1016\/0304-3975(91)90224-P","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. 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. 1\u201317. Springer (1989). https:\/\/doi.org\/10.1007\/BFB0035748, https:\/\/doi.org\/10.1007\/BFb0035748","DOI":"10.1007\/BFB0035748"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Anand, A., Mallik, K., Nayak, S.P., Schmuck, A.: Computing adequately permissive assumptions for synthesis. 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. 211\u2013228. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_15, https:\/\/doi.org\/10.1007\/978-3-031-30820-8_15","DOI":"10.1007\/978-3-031-30820-8_15"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Anand, A., Nayak, S.P., Schmuck, A.: Synthesizing permissive winning strategy templates for parity games. 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. 436\u2013458. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37706-8_22, https:\/\/doi.org\/10.1007\/978-3-031-37706-8_22","DOI":"10.1007\/978-3-031-37706-8_22"},{"key":"9_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Basset, N., Raskin, J., Sankur, O.: Admissible strategies in timed games. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 10460, pp. 403\u2013425. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_20, https:\/\/doi.org\/10.1007\/978-3-319-63121-9_20","DOI":"10.1007\/978-3-319-63121-9_20"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Belta, C., Yordanov, B., Gol, E.A.: Formal methods for discrete-time dynamical systems, vol.\u00a089. Springer (2017)","DOI":"10.1007\/978-3-319-50763-7"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. RAIRO Theor. Informatics Appl. 36(3), 261\u2013275 (2002). https:\/\/doi.org\/10.1051\/ita:2002013","DOI":"10.1051\/ita:2002013"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Berwanger, D.: Admissibility in infinite games. In: Thomas, W., Weil, P. (eds.) STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, February 22-24, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04393, pp. 188\u2013199. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-70918-3_17, https:\/\/doi.org\/10.1007\/978-3-540-70918-3_17","DOI":"10.1007\/978-3-540-70918-3_17"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Prophecy variables for hyperproperty verification. In: 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022. pp. 471\u2013485. IEEE (2022). https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658, https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Markey, N., Olschewski, J., Ummels, M.: Measuring permissiveness in parity games: Mean-payoff parity games revisited. In: Bultan, T., Hsiung, P. (eds.) Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06996, pp. 135\u2013149. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_11","DOI":"10.1007\/978-3-642-24372-1_11"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Brenguier, R., Raskin, J., Sankur, O.: Assume-admissible synthesis. Acta Informatica 54(1), 41\u201383 (2017). https:\/\/doi.org\/10.1007\/S00236-016-0273-2, https:\/\/doi.org\/10.1007\/s00236-016-0273-2","DOI":"10.1007\/S00236-016-0273-2"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Springer Nature (2021)","DOI":"10.1007\/978-3-030-72274-6"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Church, A.: Logic, arithmetic, and automata. Journal of Symbolic Logic 29(4), 210\u2013210 (1964). https:\/\/doi.org\/10.2307\/2270398","DOI":"10.2307\/2270398"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Damm, W., Finkbeiner, B.: Automatic compositional synthesis of distributed systems. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings. Lecture Notes in Computer Science, vol.\u00a08442, pp. 179\u2013193. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-06410-9_13, https:\/\/doi.org\/10.1007\/978-3-319-06410-9_13","DOI":"10.1007\/978-3-319-06410-9_13"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"van Dijk, T.: Oink: An implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10805, pp. 291\u2013308. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16, https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16","DOI":"10.1007\/978-3-319-89960-2_16"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Aisse, A.G., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From spot 2.0 to spot 2.10: What\u2019s new? In: International Conference on Computer Aided Verification, CAV 2022. Lecture Notes in Computer Science, vol. 13372. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Ehlers, R., Lafortune, S., Tripakis, S., Vardi, M.Y.: Supervisory control and reactive synthesis: a comparative introduction. Discret. Event Dyn. Syst. 27(2), 209\u2013260 (2017). https:\/\/doi.org\/10.1007\/s10626-015-0223-0","DOI":"10.1007\/s10626-015-0223-0"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B.: Synthesis of reactive systems. In: Esparza, J., Grumberg, O., Sickert, S. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol.\u00a045, pp. 72\u201398. IOS Press (2016). https:\/\/doi.org\/10.3233\/978-1-61499-627-9-72, https:\/\/doi.org\/10.3233\/978-1-61499-627-9-72","DOI":"10.3233\/978-1-61499-627-9-72"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Metzger, N., Moses, Y.: Information flow guided synthesis. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 505\u2013525. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_25, https:\/\/doi.org\/10.1007\/978-3-031-13188-2_25","DOI":"10.1007\/978-3-031-13188-2_25"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Metzger, N., Moses, Y.: Information flow guided synthesis with unbounded communication. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part III. Lecture Notes in Computer Science, vol. 14683, pp. 64\u201386. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65633-0_4, https:\/\/doi.org\/10.1007\/978-3-031-65633-0_4","DOI":"10.1007\/978-3-031-65633-0_4"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Metzger, N., Nayak, S.P., Schmuck, A.K.: Synthesis of universal safety controllers (2025), https:\/\/arxiv.org\/abs\/2501.18445","DOI":"10.1007\/978-3-031-90653-4_9"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Passing, N.: Synthesizing dominant strategies for liveness. In: Dawar, A., Guruswami, V. (eds.) 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India. LIPIcs, vol.\u00a0250, pp. 37:1\u201337:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2022.37, https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2022.37","DOI":"10.4230\/LIPICS.FSTTCS.2022.37"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Schmuck, A.K., Nayak, S.P., Metzger, N.: Artifact for synthesis of universal safety controllers at tacas 2025 (Jan 2025). https:\/\/doi.org\/10.5281\/zenodo.14627151, https:\/\/doi.org\/10.5281\/zenodo.14627151","DOI":"10.5281\/zenodo.14627151"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Fremont, D.J., Seshia, S.A.: Reactive control improvisation. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification. pp. 307\u2013326. Springer International Publishing, Cham (2018)","DOI":"10.1007\/978-3-319-96145-3_17"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Goorden, M., Fabian, M.: No synthesis needed, we are alright already. In: 2019 IEEE 15th International Conference on Automation Science and Engineering (CASE). pp. 195\u2013202 (2019). https:\/\/doi.org\/10.1109\/COASE.2019.8843071","DOI":"10.1109\/COASE.2019.8843071"},{"key":"9_CR28","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, https:\/\/doi.org\/10.48550\/arXiv.2206.00251","DOI":"10.48550\/ARXIV.2206.00251"},{"key":"9_CR29","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, https:\/\/doi.org\/10.1109\/FMCAD.2006.22","DOI":"10.1109\/FMCAD.2006.22"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Jobstmann, B., Galler, S.J., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04590, pp. 258\u2013262. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_29, https:\/\/doi.org\/10.1007\/978-3-540-73368-3_29","DOI":"10.1007\/978-3-540-73368-3_29"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Kirsten, D.: Alternating tree automata and parity games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. Lecture Notes in Computer Science, vol.\u00a02500, pp. 153\u2013167. Springer (2001). https:\/\/doi.org\/10.1007\/3-540-36387-4_9, https:\/\/doi.org\/10.1007\/3-540-36387-4_9","DOI":"10.1007\/3-540-36387-4_9"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Klein, J., Baier, C., Kl\u00fcppelholz, S.: Compositional construction of most general controllers. Acta Informatica 52(4-5), 443\u2013482 (2015). https:\/\/doi.org\/10.1007\/s00236-015-0239-9","DOI":"10.1007\/s00236-015-0239-9"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Lahijanian, M., Raman, V.: Synthesis for robots: Guarantees and feedback for robot behavior. Annual Review of Control, Robotics, and Autonomous Systems 1(1), 211\u2013236 (2018)","DOI":"10.1146\/annurev-control-060117-104838"},{"key":"9_CR34","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. In: Halbwachs, N., Peled, D.A. (eds.) Computer Aided Verification, 11th International Conference, CAV \u201999, Trento, Italy, July 6-10, 1999, Proceedings. Lecture Notes in Computer Science, vol.\u00a01633, pp. 172\u2013183. Springer (1999).https:\/\/doi.org\/10.1007\/3-540-48683-6_17, https:\/\/doi.org\/10.1007\/3-540-48683-6_17","DOI":"10.1007\/3-540-48683-6_17"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software, 10th International SPIN Workshop. Portland, OR, USA, May 9-10, 2003, Proceedings. Lecture Notes in Computer Science, vol.\u00a02648, pp. 74\u201388. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-44829-2_5, https:\/\/doi.org\/10.1007\/3-540-44829-2_5","DOI":"10.1007\/3-540-44829-2_5"},{"key":"9_CR36","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, https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25(1), 206\u2013230 (Jan 1987). https:\/\/doi.org\/10.1137\/0325013, https:\/\/doi.org\/10.1137\/0325013","DOI":"10.1137\/0325013"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Schmuck, A., Moor, T., Majumdar, R.: On the relation between reactive synthesis and supervisory control of non-terminating processes. Discret. Event Dyn. Syst. 30(1), 81\u2013124 (2020). https:\/\/doi.org\/10.1007\/s10626-019-00299-5","DOI":"10.1007\/s10626-019-00299-5"},{"key":"9_CR39","doi-asserted-by":"crossref","unstructured":"Tabuada, P.: Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media (2009)","DOI":"10.1007\/978-1-4419-0224-5"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Wonham, W., Cai, K., Rudie, K.: Supervisory control of discrete-event systems: A brief history. Annual Reviews in Control 45, 250\u2013256 (2018)","DOI":"10.1016\/j.arcontrol.2018.03.002"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Yin, X., Gao, B., Yu, X.: Formal synthesis of controllers for safety-critical autonomous systems: Developments and challenges. Annual Reviews in Control 57, 100940 (2024). https:\/\/doi.org\/10.1016\/j.arcontrol.2024.100940, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1367578824000099","DOI":"10.1016\/j.arcontrol.2024.100940"}],"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-90653-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:47Z","timestamp":1764401807000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_9","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"}}]}}