{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:51:07Z","timestamp":1742914267528,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031308192"},{"type":"electronic","value":"9783031308208"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,20]],"date-time":"2023-04-20T00:00:00Z","timestamp":1681948800000},"content-version":"vor","delay-in-days":109,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Automatic synthesis from temporal logic specifications is an attractive alternative to manual system design, due to its ability to generate correct-by-construction implementations from high-level specifications. Due to the high complexity of the synthesis problem, significant research efforts have been directed at developing practically efficient approaches for restricted specification language fragments. In this paper we focus on the  fragment of Linear Temporal Logic (LTL) syntactically <jats:italic>extended with bounded temporal operators<\/jats:italic>. We propose a new synthesis approach with the primary motivation to solve efficiently the synthesis problem for specifications with bounded temporal operators, in particular those with large bounds. The experimental evaluation of our method shows that for this type of specifications it outperforms state-of-art synthesis tools, demonstrating that it is a promising approach to efficiently treating quantitative timing constraints in safety specifications.<\/jats:p>","DOI":"10.1007\/978-3-031-30820-8_17","type":"book-chapter","created":{"date-parts":[[2023,4,19]],"date-time":"2023-04-19T19:02:36Z","timestamp":1681930956000},"page":"251-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Taming Large Bounds in Synthesis from Bounded-Liveness Specifications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5433-8133","authenticated-orcid":false,"given":"Philippe","family":"Heim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rayna","family":"Dimitrova","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,4,20]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Etessami, K., Torre, S.L., Peled, D.A.: Parametric temporal logic for \"model measuring\". ACM Trans. Comput. Log. 2(3), 388\u2013407 (2001). https:\/\/doi.org\/10.1145\/377978.377990, https:\/\/doi.org\/10.1145\/377978.377990","DOI":"10.1145\/377978.377990"},{"key":"17_CR2","doi-asserted-by":"publisher","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, https:\/\/doi.org\/10.1145\/227595.227602","DOI":"10.1145\/227595.227602"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: Time for playing games! 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. 121\u2013125. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14, https:\/\/doi.org\/10.1007\/978-3-540-73368-3_14","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Bouyer, P., Bozzelli, L., Chevalier, F.: Controller synthesis for MTL specifications. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006 - Concurrency Theory, 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings. Lecture Notes in Computer Science, vol.\u00a04137, pp. 450\u2013464. Springer (2006). https:\/\/doi.org\/10.1007\/11817949_30, https:\/\/doi.org\/10.1007\/11817949_30","DOI":"10.1007\/11817949_30"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Brihaye, T., Esti\u00e9venart, M., Geeraerts, G., Ho, H., Monmege, B., Sznajder, N.: Real-time synthesis is hard! In: Fr\u00e4nzle, M., Markey, N. (eds.) Formal Modeling and Analysis of Timed Systems - 14th International Conference, FORMATS 2016, Quebec, QC, Canada, August 24-26, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09884, pp. 105\u2013120. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-44878-7_7, https:\/\/doi.org\/10.1007\/978-3-319-44878-7_7","DOI":"10.1007\/978-3-319-44878-7_7"},{"key":"17_CR6","doi-asserted-by":"publisher","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Li, G.: Efficient controller synthesis for a fragment of mtl$$_{0,\\infty }$$. Acta Informatica 51(3-4), 165\u2013192 (2014). https:\/\/doi.org\/10.1007\/s00236-013-0189-z, https:\/\/doi.org\/10.1007\/s00236-013-0189-z","DOI":"10.1007\/s00236-013-0189-z"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Cassez, F.: Efficient on-the-fly algorithms for partially observable timed games. In: Raskin, J., Thiagarajan, P.S. (eds.) Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings. Lecture Notes in Computer Science, vol.\u00a04763, pp. 5\u201324. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-75454-1_3, https:\/\/doi.org\/10.1007\/978-3-540-75454-1_3","DOI":"10.1007\/978-3-540-75454-1_3"},{"key":"17_CR8","unstructured":"Church, A.: Logic, arithmetic and automata. In: International congress of mathematicians. pp. 23\u201335 (1962)"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Geatti, L., Gigante, N., Montanari, A., Tonetta, S.: Reactive synthesis from extended bounded response LTL specifications. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020. pp. 83\u201392. IEEE (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_15, https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_15","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_15"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal stratego. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. Lecture Notes in Computer Science, vol.\u00a09035, pp. 206\u2013211. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16, https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16","DOI":"10.1007\/978-3-662-46681-0_16"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Doyen, L., Geeraerts, G., Raskin, J., Reichert, J.: Realizability of real-time logics. In: Ouaknine, J., Vaandrager, F.W. (eds.) Formal Modeling and Analysis of Timed Systems, 7th International Conference, FORMATS 2009, Budapest, Hungary, September 14-16, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05813, pp. 133\u2013148. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04368-0_12, https:\/\/doi.org\/10.1007\/978-3-642-04368-0_12","DOI":"10.1007\/978-3-642-04368-0_12"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"D\u2019Souza, D., Madhusudan, P.: Timed control synthesis for external specifications. In: Alt, H., Ferreira, A. (eds.) STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes - Juan les Pins, France, March 14-16, 2002, Proceedings. Lecture Notes in Computer Science, vol.\u00a02285, pp. 571\u2013582. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45841-7_47, https:\/\/doi.org\/10.1007\/3-540-45841-7_47","DOI":"10.1007\/3-540-45841-7_47"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Heim, P., Dimitrova, R.: Taming large bounds in synthesis from bounded-liveness specifications (full version) (2023). https:\/\/doi.org\/10.48550\/ARXIV.2301.10032, https:\/\/arxiv.org\/abs\/2301.10032","DOI":"10.48550\/ARXIV.2301.10032"},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"Hofmann, T., Schupp, S.: Tacos: A tool for MTL controller synthesis. In: Calinescu, R., Pasareanu, C.S. (eds.) Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings. Lecture Notes in Computer Science, vol. 13085, pp. 372\u2013379. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_21, https:\/\/doi.org\/10.1007\/978-3-030-92124-8_21","DOI":"10.1007\/978-3-030-92124-8_21"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Koymans, R.: Specifying real-time properties with metric temporal logic. Real Time Syst. 2(4), 255\u2013299 (1990). https:\/\/doi.org\/10.1007\/BF01995674, https:\/\/doi.org\/10.1007\/BF01995674","DOI":"10.1007\/BF01995674"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robotics 25(6), 1370\u20131381 (2009). https:\/\/doi.org\/10.1109\/TRO.2009.2030225, https:\/\/doi.org\/10.1109\/TRO.2009.2030225","DOI":"10.1109\/TRO.2009.2030225"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Formal Methods Syst. Des. 34(2), 83\u2013103 (2009). https:\/\/doi.org\/10.1007\/s10703-009-0067-z, https:\/\/doi.org\/10.1007\/s10703-009-0067-z","DOI":"10.1007\/s10703-009-0067-z"},{"key":"17_CR18","doi-asserted-by":"publisher","unstructured":"Li, G., Jensen, P.G., Larsen, K.G., Legay, A., Poulsen, D.B.: Practical controller synthesis for mtl$$_{0,\\,\\,\\infty }$$. In: Erdogmus, H., Havelund, K. (eds.) Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, Santa Barbara, CA, USA, July 10-14, 2017. pp. 102\u2013111. ACM (2017). https:\/\/doi.org\/10.1145\/3092282.3092303, https:\/\/doi.org\/10.1145\/3092282.3092303","DOI":"10.1145\/3092282.3092303"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica 57(1-2), 3\u201336 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00349-3, https:\/\/doi.org\/10.1007\/s00236-019-00349-3","DOI":"10.1007\/s00236-019-00349-3"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: On synthesizing controllers from bounded-response properties. 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. 95\u2013107. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_12, https:\/\/doi.org\/10.1007\/978-3-540-73368-3_12","DOI":"10.1007\/978-3-540-73368-3_12"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). 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. 229\u2013242. Springer (1995). https:\/\/doi.org\/10.1007\/3-540-59042-0_76, https:\/\/doi.org\/10.1007\/3-540-59042-0_76","DOI":"10.1007\/3-540-59042-0_76"},{"key":"17_CR22","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, https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Nickovic, D., Piterman, N.: From mtl to deterministic timed automata. In: Chatterjee, K., Henzinger, T.A. (eds.) Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06246, pp. 152\u2013167. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15297-9_13, https:\/\/doi.org\/10.1007\/978-3-642-15297-9_13","DOI":"10.1007\/978-3-642-15297-9_13"},{"key":"17_CR24","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":"17_CR25","doi-asserted-by":"publisher","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A symbolic approach to safety LTL synthesis. In: Strichman, O., Tzoref-Brill, R. (eds.) Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10629, pp. 147\u2013162. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10, https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10","DOI":"10.1007\/978-3-319-70389-3_10"}],"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-30820-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:05:30Z","timestamp":1690974330000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30820-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308192","9783031308208"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30820-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"20 April 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}