{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:35:58Z","timestamp":1784241358973,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study semi-algorithms to synthesise the constraints under which a Parametric Timed Automaton satisfies some liveness requirement. The algorithms traverse a possibly infinite parametric zone graph, searching for accepting cycles. We provide new search and pruning algorithms, leading to successful termination for many examples. We demonstrate the success and efficiency of these algorithms on a benchmark. We also illustrate parameter synthesis for the classical Bounded Retransmission Protocol. Finally, we introduce a new notion of completeness in the limit, to investigate if an algorithm enumerates all solutions.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_17","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T22:03:37Z","timestamp":1616191417000},"page":"311-329","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8473-9555","authenticated-orcid":false,"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3019-4902","authenticated-orcid":false,"given":"Jaime","family":"Arias","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3154-5268","authenticated-orcid":false,"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-0625","authenticated-orcid":false,"given":"Jaco van de","family":"Pol","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"17_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"17_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Kosaraju, S.R., Johnson, D.S., Aggarwal, A. (eds.) STOC. pp. 592\u2013601. ACM, New York, NY, USA (1993). https:\/\/doi.org\/10.1145\/167088.167242","DOI":"10.1145\/167088.167242"},{"key":"17_CR3","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9.: What\u2019s decidable about parametric timed automata? International Journal on Software Tools for Technology Transfer (2019). https:\/\/doi.org\/10.1007\/s10009-017-0467-0","DOI":"10.1007\/s10009-017-0467-0"},{"key":"17_CR4","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9.: A benchmark library for parametric timed model checking. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS. Communications in Computer and Information Science, vol.\u00a01008, pp. 75\u201383. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-12988-0_5","DOI":"10.1007\/978-3-030-12988-0_5"},{"key":"17_CR5","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Chatain, Th., Encrenaz, E., Fribourg, L.: An inverse method for parametric timed automata. International Journal of Foundations of Computer Science 20(5), 819\u2013836 (2009). https:\/\/doi.org\/10.1142\/S0129054109006905","DOI":"10.1142\/S0129054109006905"},{"key":"17_CR6","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., K\u00fchne, U., Soulat, R.: IMITATOR\u00a02.5: A\u00a0tool for analyzing robustness in scheduling problems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM. Lecture Notes in Computer Science, vol.\u00a07436, pp. 33\u201336. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_6","DOI":"10.1007\/978-3-642-32759-9_6"},{"key":"17_CR7","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Fribourg, L., Soulat, R.: Merge and conquer: State merging in parametric timed automata. In: Hung, D.V., Ogawa, M. (eds.) ATVA. Lecture Notes in Computer Science, vol.\u00a08172, pp. 381\u2013396. Springer (Oct 2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_27","DOI":"10.1007\/978-3-319-02444-8_27"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Lime, D.: Liveness in L\/U-parametric timed automata. In: Legay, A., Schneider, K. (eds.) ACSD. pp. 9\u201318. IEEE (2017). https:\/\/doi.org\/10.1109\/ACSD.2017.19","DOI":"10.1109\/ACSD.2017.19"},{"key":"17_CR9","doi-asserted-by":"publisher","unstructured":"Andr\u00e9, \u00c9., Nguyen, H.G., Petrucci, L., Sun, J.: Parametric model checking timed automata under non-Zenoness assumption. In: Barrett, C., Kahsai, T. (eds.) NFM. Lecture Notes in Computer Science, vol. 10227, pp. 35\u201351. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_3","DOI":"10.1007\/978-3-319-57288-8_3"},{"key":"17_CR10","doi-asserted-by":"publisher","unstructured":"Bagnara, R., M., H.P., Zaffanella, E.: The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Science of Computer Programming 72(1\u20132), 3\u201321 (2008). https:\/\/doi.org\/10.1016\/j.scico.2007.08.001","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"17_CR11","doi-asserted-by":"publisher","unstructured":"Bezd\u011bk, P., Bene\u0161, N., Barnat, J., \u010cern\u00e1, I.: LTL parameter synthesis of parametric timed automata. In: Nicola, R.D., eva K\u00fchn (eds.) SEFM. Lecture Notes in Computer Science, vol.\u00a09763, pp. 172\u2013187. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_12","DOI":"10.1007\/978-3-319-41591-8_12"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Magnago, E.: Proving the existence of fair paths in infinite-state systems. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI. Lecture Notes in Computer Science, vol. 12597, pp. 104\u2013126. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_6","DOI":"10.1007\/978-3-030-67067-2_6"},{"key":"17_CR13","doi-asserted-by":"publisher","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1(2\/3), 275\u2013288 (1992). https:\/\/doi.org\/10.1007\/BF00121128","DOI":"10.1007\/BF00121128"},{"key":"17_CR14","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Katoen, J.P., Ruys, T.C., Tretmans, J.: The bounded retransmission protocol must be on time! In: Brinksma, E. (ed.) TACAS. Lecture Notes in Computer Science, vol.\u00a01217, pp. 416\u2013431. Springer (1997). https:\/\/doi.org\/10.1007\/BFb0035403","DOI":"10.1007\/BFb0035403"},{"key":"17_CR15","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 A framework for LTL and $$\\omega $$-automata manipulation. In: ATVA. Lecture Notes in Computer Science, vol.\u00a09938, pp. 122\u2013129. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"17_CR16","doi-asserted-by":"publisher","unstructured":"Groote, J.F., van\u00a0de Pol, J.: A bounded retransmission protocol for large data packets. In: Wirsing, M., Nivat, M. (eds.) AMAST. Lecture Notes in Computer Science, vol.\u00a01101, pp. 536\u2013550. Springer (1996). https:\/\/doi.org\/10.1007\/BFb0014338","DOI":"10.1007\/BFb0014338"},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Herbreteau, F., Srivathsan, B.: Efficient on-the-fly emptiness check for timed B\u00fcchi automata. In: Bouajjani, A., Chin, W.N. (eds.) ATVA. Lecture Notes in Computer Science, vol.\u00a06252, pp. 218\u2013232. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_17","DOI":"10.1007\/978-3-642-15643-4_17"},{"key":"17_CR18","doi-asserted-by":"publisher","unstructured":"Herbreteau, F., Srivathsan, B., Tran, T.T., Walukiewicz, I.: Why liveness for timed automata is hard, and what we can do about it. ACM Transactions on Computational Logic 21(3), 17:1\u201317:28 (2020). https:\/\/doi.org\/10.1145\/3372310","DOI":"10.1145\/3372310"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 52-53, 183\u2013220 (2002). https:\/\/doi.org\/10.1016\/S1567-8326(02)00037-1","DOI":"10.1016\/S1567-8326(02)00037-1"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Jovanovi\u0107, A., Lime, D., Roux, O.H.: Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engineering 41(5), 445\u2013461 (2015). https:\/\/doi.org\/10.1109\/TSE.2014.2357445","DOI":"10.1109\/TSE.2014.2357445"},{"key":"17_CR21","doi-asserted-by":"publisher","unstructured":"Knapik, M., Penczek, W.: Bounded model checking for parametric timed automata. Transactions on Petri Nets and Other Models of Concurrency 5, 141\u2013159 (2012). https:\/\/doi.org\/10.1007\/978-3-642-29072-5_6","DOI":"10.1007\/978-3-642-29072-5_6"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van\u00a0de Pol, J.: Multi-core emptiness checking of timed B\u00fcchi automata using inclusion abstraction. In: Sharygina, N., Veith, H. (eds.) CAV. Lecture Notes in Computer Science, vol.\u00a08044, pp. 968\u2013983. Springer, Heidelberg, Germany (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_69","DOI":"10.1007\/978-3-642-39799-8_69"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Li, G.: Checking timed B\u00fcchi automata emptiness using LU-abstractions. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS, Lecture Notes in Computer Science, vol.\u00a05813, pp. 228\u2013242. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-04368-0_18","DOI":"10.1007\/978-3-642-04368-0_18"},{"key":"17_CR24","doi-asserted-by":"publisher","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS. Lecture Notes in Computer Science, vol.\u00a04202, pp. 274\u2013289. Springer (2006). https:\/\/doi.org\/10.1007\/11867340_20","DOI":"10.1007\/11867340_20"},{"key":"17_CR25","doi-asserted-by":"publisher","unstructured":"Nguyen, H.G., Petrucci, L., van\u00a0de Pol, J.: Layered and collecting NDFS with subsumption for parametric timed automata. In: Lin, A.W., Sun, J. (eds.) ICECCS. pp.\u00a01\u20139. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/ICECCS2018.2018.00009","DOI":"10.1109\/ICECCS2018.2018.00009"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"van\u00a0de Pol, J., Petrucci, L.: On completeness of liveness synthesis for parametric timed automata (extended abstract, invited talk). In: Roggenbach, M. (ed.) WADT 2020 (2021), to appear","DOI":"10.1007\/978-3-030-73785-6_1"},{"key":"17_CR27","doi-asserted-by":"publisher","unstructured":"Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed B\u00fcchi automata emptiness efficiently. Formal Methods in System Design 26(3), 267\u2013292 (2005). https:\/\/doi.org\/10.1007\/s10703-005-1632-8","DOI":"10.1007\/s10703-005-1632-8"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72016-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,29]],"date-time":"2021-04-29T20:36:24Z","timestamp":1619728584000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","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":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"141","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":"41","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":"21","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":"29% - 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":"12","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)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}